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) |