Program

Friday Room 2405
	8:00 to 8:30	Breakfast
	8:30 to 8:40	Opening Remarks (Mahesh Viswanathan)
8:40 to 10:40: Aws Albarghouthi
	Ashutosh Trivedi	Skolem functions for factored formulas (abstract)
	Alain Mebsout	Certificates for the model checker Kind 2 (abstract)
	Benjamin Susman	Constraint Answer Set Programming versus Satisfiability Modulo Theories Or Constraints versus Theories (abstract)
	Adam Procter	Mechanizing metatheory of rewire (abstract)
	10:40 to 11:00	Coffee Break
11:00 to 12:00: Mahesh Viswanathan
	Rance Cleaveland	Keynote: Prove If You Can, Test If You Cannot (abstract)
	12:00 to 1:30	Lunch
1:30 to 3:30: Ashutosh Trivedi
	Yu Wang	A Mori-Zwanzig and MITL Based Approach to Statistical Verification of Continuous-time Dynamical Systems (abstract)
	Chuchu Fan	Bounded verification using on the fly discrepancy computation (abstract)
	Sergio Mover	Verifying LTL properties of hybrid systems with K-LIVENESS (abstract)
	Pavithra Prabhakar	Non-zenoness verification to termination (abstract)
	3:30 to 3:50	Coffee Break
3:50 to 5:50: Loris d’Antoni
	Gowtham Kaki	Infering consistency specifications from tests (abstract)
	Shawn Meier	Generating ordering Constraints on Android Applications Callbacks (abstract)
	Wing Lam	Parameterized Unit Testing in the Wild (abstract)
	Shambwaditya Saha	NetGen: Synthesizing data-plane configurations for network policies (abstract)
Saturday Room 0216
	8:00 to 8:30	Breakfast
8:30 to 10:00: Andrew Miner
	David Greve	Keynote: Analyzing Information Flow Properties of C Programs (abstract)
	Umang Mathur	Using Symbolic Model Checking for Computing Information Flow (abstract)
	10:00 to 10:20	Coffee Break
10:20 to 12:20: Rohit Chadha
	Philip Daian	Runtime verification: Techniques, Applications and Examples (abstract)
	Andrey Yavolovsky	Decision-Theoretic monitoring of cyber-physical systems (abstract)
	Mehdi Bagherzadeh	Concurrent programming with modular reasoning (abstract)
	Angello Astorga	Automatic Precondition Generation for repairing runtime errors (abstract)