CAV 2007

Computer Aided Verification (CAV)

19th International Conference

July 3-7, 2007, Berlin, Germany


Schedule for Saturday, July 7

Back to CAV Schedule

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


Back to CAV Schedule.