Time | | |
| | |
08:45-09:00 | | Welcome |
| | Holger Hermanns, Werner Damm
Welcome to CAV 2007 |
| | |
09:00-10:00 | | Invited Talk
Chair: Holger Hermanns |
| |
Byron Cook
Automatically Proving Program Termination
|
| | |
10:00-10:30 | | Coffee Break |
| | |
10:30-11:30 | | Session I: Compositionality
Session Chair: Bob R. Kurshan
|
|
10:30-11:00
|
Nishant Sinha and Edmund Clarke
SAT-based Compositional Verification using Lazy Learning
|
| | |
| 11:00-11:30 | Ariel Cohen and Kedar Namjoshi
Local Proofs for Global Safety Properties |
| | |
11:30-12:30 | | Session II: Verification Process
Session Chair: Parosh Abdulla |
|
11:30-12:00
|
Denis Gopan and Thomas Reps
Low-Level Library Analysis and Summarization
|
| | |
| 12:00-12:30 | Sagar Chaki, Christian Schallhart and Helmut Veith
Verification Across Intellectual Property Boundaries |
| | |
12:30-14:00 | | Lunch Break |
| | |
14:00-15:30 | | Session III: Timed Synthesis and Games
Session Chair: Roderick Bloem |
|
14:00-14:30
|
Oded Maler, Dejan Nickovic and Amir Pnueli
On Synthesizing Controllers from Bounded-Response Properties
|
| | |
| 14:30-15:00 | Luca de Alfaro and Marco Faella
An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games |
| | |
| 15:00-15:15 | Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury,
Kim G. Larsen and Didier Lime
Uppaal-Tiga: Time for Playing Games! |
| | |
| 15:15-15:30 | Martin Ouimet and Kristina Lundqvist
The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems |
| | |
15:30-16:00 | | Coffee Break |
| | |
16:00-17:00 | | Session IV: Infinite State Verification
Session Chair: Rajeev Alur |
|
16:00-16:30
|
Mayank Saksena and Bengt Jonsson
Systematic Acceleration in Regular Model Checking
|
| | |
| 16:30-17:00 | Ahmed Rezine, Parosh Abdulla and Giorgio Delzanno
Parameterized Verification of Infinite-state Processes with Global Conditions |
| | |
17:00-18:00 | | Session V: Tool Environments
Session Chair: Alessandro Cimatti |
|
17:00-17:15
|
Hubert Garavel, Radu Mateescu, Frédéric Lang and Wendelin Serwe
CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes
|
| | |
| 17:15-17.30 | Dejvuth Suwimonteerabuth, Felix Berger, Stefan Schwoon
and Javier Esparza
jMoped: A Test Environment for Java programs |
| | |
| 17:30-17:45 | Nathaniel Charlton and Michael Huth
Hector: software model checking with cooperating analysis plugins |
| | |
| 17:45-18:00 | Jean-Christophe Filliatre and Claude Marché
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification |
| | |
20:00-open | | PC-Dinner (PC- and SC-Members only) |
