Time | | | | | |
| | | | | |
09:00-10:00 | | Session XIII: Assume-Guarantee Reasoning
Chair: Orna Grumberg | | | |
|
09:00-09:30
|
Orna Kupferman, Nir Piterman and Moshe Vardi
From Liveness to Promptness
| | | |
| | | | | |
| 09:30-10:00 | Anubhav Gupta, Ken McMillan and Zhaohui Fu
Automated Assumption Generation for Compositional Verification | | | |
| | | | | |
10:00-10:30 | | Coffee Break | | | |
| | | | | |
10:30-12:00 | | Session XIV: Hybrid Systems
Session Chair: Werner Damm | | | |
|
10:30-11:00
|
Marc Segelken
Abstraction and Counterexample-guided Construction of omega-Automata for Model Checking of Step-discrete linear Hybrid Models
| | | |
| | | | | |
| 11:00-11:30 | Tarik Nahhal and Thao Dang
Test Coverage for Continuous and Hybrid Systems | | | |
| | | | | |
| 11:30-12:00 | Erion Plaku, Lydia Kavraki and Moshe Vardi
Hybrid Systems: From Verification to Falsification | | | |
| | | | | |
12:00-12:30 | | Presentation: HW Model Checking Competition
Armin Biere and Toni Jussila | | | |
| | | | | |
12:30-14:00 | | Lunch Break | | | |
| | | | | |
14:00-14:15 | | Presentation: SMT Competition
Clark Barrett, Albert Oliveras, and Morgan Deters | | | |
| | | | | |
14:15-15:45 | | Session XV: Program Analysis
Session Chair: Ahmed Bouajjani | | | |
|
14:15-14:45
|
Daphna Amit, Noam Rinetzky, Thomas Reps, Mooly Sagiv and Eran Yahav
Comparison under Abstraction for Verifying Linearizability
| | | |
| | | | | |
| 14:45-15:15 | Thomas Ball, Orna Kupferman and Mooly Sagiv
Leaping Loops in the Presence of Abstraction | | | |
| | | | | |
| 15:15-15:45 | Dirk Beyer, Thomas A. Henzinger and Grégory Théoduloz
Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis | | | |
| | | | | |
15:45-16:15 | | Coffee Break | | | |
| | | | | |
16:15-17:45 | | Session XVI: SAT Decision Procedures
Session Chair: Fabio Somenzi | | | |
|
16:15-16:45
|
Vijay Ganesh and David Dill
A Decision Procedure for Bit-Vectors and Arrays
| | | |
| | | | | |
| 16:45-17:15 | Alessandro Cimatti, Marco Roveri, Viktor Schuppan and Stefano Tonetta
Boolean Abstraction for Temporal Logic Satisfiability | | | |
| | | | | |
| 17:15-17:45 | Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti and Roberto Sebastiani
A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification Problems | | | |
| | | | | |
17:45-18:00 | | End | | | |
| | Holger Hermanns, Werner Damm | | | |
