CAV program

Sessions take place in auditorium 1 unless otherwise indicated.

Saturday July 27th

Saturday's program is also available with abstracts or side by side with other meetings.

09:00-11:15  Session 1: Tutorial I
Chair: Kim Guldstrand Larsen

09:00  Wolfgang Thomas, Aachen U of Techn., Germany
Invited tutorial: Infinite games and verification
10:00  Coffee Break
10:15  Wolfgang Thomas, Aachen U of Techn., Germany
continued: Infinite games and verification

11:30-12:30  Session 2: Tutorial IIa
Chair: Ed Brinksma

11:30  Patrick Cousot, ENS Paris, France
Invited tutorial: On abstraction in software verification

12:30-14:00  Lunch

14:00-15:00  Session 3: Tutorial IIb
Chair: Ed Brinksma

14:00  Patrick Cousot, ENS Paris, France
continued: On abstraction in software verification

15:15-17:30  Session 4: Tutorial III
Chair: Jens Chr. Godskesen

15:15  Thomas A. Henzinger, U California-Berkeley, USA
Invited tutorial: The symbolic approach to hybrid systems
16:15  Coffee Break
16:30  Thomas A. Henzinger, U California-Berkeley, USA
continued: The symbolic approach to hybrid systems

17:30-19:00  Welcome reception (joint with CADE)
Room: Lobby

Sunday July 28th

Sunday's program is also available with abstracts or side by side with other meetings.

08:45-10:30  Session 5: Symbolic Model Checking I
Chair: Edmund M. Clarke

08:45  Introduction and Welcome
09:00  Sharon Barner, Daniel Geist, and Anna Gringauze; IBM Haifa, Israel
Symbolic localization reduction with reconstruction layering and backtracking
09:30  Randal E. Bryant, Shuvendu K. Lahiri, and Sanjit A. Seshia; Carnegie Mellon U, USA
Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions
10:00  Sharon Barner, IBM Haifa, Israel and Orna Grumberg, Israel Inst. of Techn.
Combining symmetry reduction and under-approximation for symbolic model checking

10:30-11:00  Refreshments

11:00-12:30  Session 6: Abstraction and Refinement
Chair: Robert Kurshan

11:00  Amir Pnueli, Weizmann Inst. of Science, Israel; Jessie Xu, New York U, USA; and Lenore Zuck, New York U, USA
Liveness with (0,1,infinity)-counter abstraction
11:30  Prosenjit Chatterjee, Hemanthkumar Sivaraj, and Ganesh Gopalakrishnan; U Utah, USA
Shared memory consistency protocol verification against weak memory models: refinement via model-checking
12:00  Patrice Godefroid, Bell Labs, USA and Radha Jagadeesan, Loyola U Chicago, USA
Automatic abstraction using generalized model checking

12:30-14:00  Lunch

14:00-15:30  Session 7: Compositional Verification I
Chair: Thomas A. Henzinger

14:00  Jason Baumgartner, IBM Enterprise Systems Group, USA; Andreas Kuehlmann, Cadence Design Systems, USA; and Jacob Abraham, U Texas-Austin, USA
Property checking via structural analysis
14:30  Sriram K. Rajamani and Jakob Rehof, Microsoft Research, USA
Conformance checking for models of asynchronous message passing software
15:00  Cormac Flanagan, Shaz Qadeer, and Sanjit Seshia; Compaq, USA
A modular checker for multithreaded programs

15:30-16:00  Refreshments

16:00-17:30  Session 8: Timing Analysis
Chair: Doron A. Peled

16:00  Tomohiro Yoneda, Tokyo Inst. of Techn., Japan; Tomoya Kitai, Tokyo Inst. of Techn., Japan; and Chris Myers, U Utah, USA
Automatic derivation of timing constraints by failure analysis
16:30  Ofer Strichman, Sanjit A. Seshia, and Randal E. Bryant; Carnegie Mellon U, USA
Reducing linear inequalities to propositional formulas
17:00  Hakan L. S. Younes and Reid G. Simmons, Carnegie Mellon U, USA
Probabilistic verification of descrete event systems using acceptance sampling

Monday July 29th

Monday's program is also available with abstracts or side by side with other meetings.

09:00-10:00  Invited talk (joint with CADE)

09:00  Sharad Malik, Princeton U, USA
Invited talk: The quest for efficient Boolean satisfiability solvers

10:00-10:30  Session 9: SAT Based Methods I

10:00  Clark W. Barrett, David L. Dill, and Aaron Stump; Stanford U, USA
Checking satisfiability of first-order formulas by incremental translation to SAT

10:30-11:00  Refreshments

11:00-12:30  Session 10: SAT Based Methods II
Chair: David Basin

11:00  Ken L. McMillan, Cadence Design Systems, USA
Applying SAT methods in unbounded symbolic model checking
11:30  Edmund M. Clarke, Carnegie Mellon U, USA; Anubhav Gupta, Carnegie Mellon U, USA; James Kukula, Synopsis, USA; and Ofer Strichman, Carnegie Mellon U, USA
SAT based abstraction-refinement using ILP and machine learning techniques
12:00  Jesse D. Bingham and Alan J. Hu, U British Columbia, Canada
Semi-formal bounded model checking

12:30-14:00  Lunch

14:00-15:30  Session 11: Symbolic Model Checking II
Chair: Ken McMillan

14:00  Marco Bozzano, ITC-irst, Italy and Giorgio Delzanno, U Genova, Italy
Algorithmic verification of invalidation-based protocols
14:30  Christian Jacobi, Saarland U, Germany
Formal verification of complex out-of-order pipelines by combining model-checking and theorem-proving
15:00  Yannick Chevalier and Laurent Vigneron, LORIA Nancy, France
Automated unbounded verification of security protocols

15:30-16:00  Refreshments

16:00-17:30  Session 12: Tool Presentations I
Chair: Armin Biere

16:00  Rajeev Alur, Michael McDougall, and Zijiang Yang; U Pennsylvania, USA
Exploiting behavioral hierarchy for efficient model checking
16:15  Marius Bozga, Susanne Graf, and Laurent Mounier; IMAG Grenoble, France
IF-2.0: A validation environment for component-based real-time systems
16:30  Alessandro Armando, U Genova, Italy et al.
The AVISS security protocols analysis tool
16:45  Eugene Asarin, IMAG Grenoble, France; Gordon Pace, INRIA Rhône-Alpes, France; Gerardo Schneider, IMAG Grenoble, France; and Sergio Yovine, IMAG Grenoble, France
SPeeDI - a verification tool for polygonal hybrid systems
17:00  Alessandro Cimatti, ITC-irst, Italy et al.
NuSMV2: an opensource tool for symbolic model checking
17:15  Eugene Asarin, Thao Dang, and Oded Maler; IMAG Grenoble, France
The d/dt tool for verification of hybrid systems

19:00-21:00  City Hall reception (joint with CADE, ICLP, TABLEAUX)
Room: City Hall

Tuesday July 30th

Tuesday's program is also available with abstracts or side by side with other meetings.

09:00-10:30  Session 13: Infinite State Model Checking
Chair: Fabio Somenzi

09:00  Orna Kupferman, Hebrew U of Jerusalem, Israel; Nir Piterman, Weizmann Inst. of Science, Israel; and Moshe Y. Vardi, Rice U, USA
Model checking linear properties of prefix-recognizable systems
09:30  Tatiana Rybina and Andrei Voronkov, U Manchester, UK
Using canonical representations of solutions to speed up infinite-state model checking
10:00  Walter Hartong, Lars Hedrich, and Erich Barke; U Hannover, Germany
On discrete modeling and model checking for nonlinear analog systems

10:30-11:00  Refreshments

11:00-12:30  Session 14: Compositional Verification II
Chair: Joseph Sifakis

11:00  Arindam Chakrabarti, U California-Berkeley, USA; Luca de Alfaro, U California-Santa Cruz, USA; Thomas A. Henzinger, U California-Berkeley, USA; and Freddy Y. C. Mang, U California-Berkeley, USA
Synchronous and bidirectional component interfaces
11:30  Arindam Chakrabarti, U California-Berkeley, USA; Luca de Alfaro, U California-Santa Cruz, USA; Thomas A. Henzinger, U California-Berkeley, USA; Marcin Jurdzinski, U California-Berkeley, USA; and Freddy Y. C. Mang, U California-Berkeley, USA
Interface compatibility checking for software objects
12:00  Michael A. Colón and Henny B. Sipma, Stanford U, USA
Practical methods for proving program termination

12:30-14:00  Lunch

14:00-15:30  Session 15: Extended Model Checking
Chair: Gerard J. Holzmann

14:00  Li Tan and Rance Cleaveland, State U of New York-Stony Brook, USA
Evidence-based model checking
14:30  Gianpiero Cabodi, Sergio Nocco, and Stefano Quer; Polytechnic of Turin, Italy
Mixing forward and backward traversals in guided-prioritized BDD-based verification
15:00  Mitra Purandare and Fabio Somenzi, U Colorado-Boulder, USA
Vacuum cleaning CTL formulae

15:30-16:00  Refreshments

16:00-17:15  Session 16: Tool Presentations II
Chair: Natarajan Shankar

16:00  Aaron Stump, Clark W. Barrett, and David L. Dill; Stanford U, USA
CVC: a cooperating validity checker
16:15  Marsha Chechik, Benet Devereux, and Arie Gurfinkel; U Toronto, Canada
ξChek: A multi-valued model-checker
16:30  Shoham Ben-David, Anna Gringauze, Baruch Sterin, and Yaron Wolfsthal; IBM Haifa, Israel
PathFinder: A tool for design exploration
16:45  Dennis Dams, Bell Labs, USA; William Hesse, U Massachusetts, USA; and Gerard J. Holzmann, Bell Labs, USA
Abstracting C with abC
17:00  Alex Groce, Carnegie Mellon U, USA; Doron A. Peled, U Texas-Austin, USA; and Mihalis Yannakakis, Avaya Laboratories, USA
AMC: An adaptive model checker

17:15-18:15  CAV Business Meeting

19:30-22:00  Conference dinner
Room: Restaurant Luftkastellet

Wednesday July 31st

Wednesday's program is also available with abstracts or side by side with other meetings.

09:00-10:00  Session 17: Invited talk
Chair: Ed Brinksma

09:00  Gerard J. Holzmann, Bell Labs, USA
Invited talk: Software analysis and model checking

10:00-10:30  Session 18: Code Verification

10:00  Thomas A. Henzinger, U California-Berkeley, USA; Ranjit Jhala, U California-Berkeley, USA; Rupak Majumdar, U California-Berkeley, USA; George C. Necula, U California-Berkeley, USA; Grégoire Sutre, LaBRI Bordeaux, France; and Westley Weimer, U California-Berkeley, USA
Temporal-safety proofs for systems code

10:30-11:00  Refreshments

11:00-12:30  Session 19: Regular Model Checking
Chair: Amir Pnueli

11:00  Ahmed Bouajjani and Tayssir Touili, U Paris VII, France
Extrapolating tree transformations
11:30  Parosh Aziz Abdulla, Bengt Jonsson, Pritha Mahata, and Julien d'Orso; Uppsala U, Sweden
Regular tree model checking
12:00  Robert Kurshan, Cadence Design Systems, USA; Vladimir Levin, Bell Labs, USA; and Husnu Yenigun, Sebancy U, Turkey
Compressing transitions for model checking

12:30-14:00  Lunch

14:00-15:30  Session 20: Model Reduction
Chair: Kim Guldstrand Larsen

14:00  Victor Khomenko, U Newcastle upon Tyne, UK; Maciej Koutny, U Newcastle upon Tyne, UK; and Walter Vogler, U Augsburg, Germany
Canonical prefixes of Petri net unfoldings
14:30  Stefan Blom and Jaco van de Pol, CWI Amsterdam, The Netherlands
State space reduction by proving confluence
15:00  Sankar Gurumurthy, U Colorado-Boulder, USA; Roderick Bloem, Graz U of Techn., Austria; and Fabio Somenzi, U Colorado-Boulder, USA
Fair simulation minimization