![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
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 |
| FLoC |
|
| MEETINGS |
|
| PROGRAM |
|
| FACILITIES |
|
| COPENHAGEN |
|
| MISCELLANEOUS |
|
