Regular papers

Parosh Aziz Abdulla, Bengt Jonsson, Pritha Mahata, and Julien d'Orso; Uppsala U, Sweden
Regular tree model checking

Rajeev Alur, Michael McDougall, and Zijiang Yang; U Pennsylvania, USA
Exploiting behavioral hierarchy for efficient model checking

Alessandro Armando, U Genova, Italy et al.
The AVISS security protocols analysis tool

Eugene Asarin, Thao Dang, and Oded Maler; IMAG Grenoble, France
The d/dt tool for verification of hybrid systems

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

Sharon Barner, Daniel Geist, and Anna Gringauze; IBM Haifa, Israel
Symbolic localization reduction with reconstruction layering and backtracking

Sharon Barner, IBM Haifa, Israel and Orna Grumberg, Israel Inst. of Techn.
Combining symmetry reduction and under-approximation for symbolic model checking

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

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

Shoham Ben-David, Anna Gringauze, Baruch Sterin, and Yaron Wolfsthal; IBM Haifa, Israel
PathFinder: A tool for design exploration

Jesse D. Bingham and Alan J. Hu, U British Columbia, Canada
Semi-formal bounded model checking

Stefan Blom and Jaco van de Pol, CWI Amsterdam, The Netherlands
State space reduction by proving confluence

Ahmed Bouajjani and Tayssir Touili, U Paris VII, France
Extrapolating tree transformations

Marius Bozga, Susanne Graf, and Laurent Mounier; IMAG Grenoble, France
IF-2.0: A validation environment for component-based real-time systems

Marco Bozzano, ITC-irst, Italy and Giorgio Delzanno, U Genova, Italy
Algorithmic verification of invalidation-based protocols

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

Gianpiero Cabodi, Sergio Nocco, and Stefano Quer; Polytechnic of Turin, Italy
Mixing forward and backward traversals in guided-prioritized BDD-based verification

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

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

Prosenjit Chatterjee, Hemanthkumar Sivaraj, and Ganesh Gopalakrishnan; U Utah, USA
Shared memory consistency protocol verification against weak memory models: refinement via model-checking

Marsha Chechik, Benet Devereux, and Arie Gurfinkel; U Toronto, Canada
ξChek: A multi-valued model-checker

Yannick Chevalier and Laurent Vigneron, LORIA Nancy, France
Automated unbounded verification of security protocols

Alessandro Cimatti, ITC-irst, Italy et al.
NuSMV2: an opensource tool for symbolic model checking

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

Michael A. Colón and Henny B. Sipma, Stanford U, USA
Practical methods for proving program termination

Dennis Dams, Bell Labs, USA; William Hesse, U Massachusetts, USA; and Gerard J. Holzmann, Bell Labs, USA
Abstracting C with abC

Cormac Flanagan, Shaz Qadeer, and Sanjit Seshia; Compaq, USA
A modular checker for multithreaded programs

Patrice Godefroid, Bell Labs, USA and Radha Jagadeesan, Loyola U Chicago, USA
Automatic abstraction using generalized model checking

Alex Groce, Carnegie Mellon U, USA; Doron A. Peled, U Texas-Austin, USA; and Mihalis Yannakakis, Avaya Laboratories, USA
AMC: An adaptive model checker

Sankar Gurumurthy, U Colorado-Boulder, USA; Roderick Bloem, Graz U of Techn., Austria; and Fabio Somenzi, U Colorado-Boulder, USA
Fair simulation minimization

Walter Hartong, Lars Hedrich, and Erich Barke; U Hannover, Germany
On discrete modeling and model checking for nonlinear analog systems

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

Christian Jacobi, Saarland U, Germany
Formal verification of complex out-of-order pipelines by combining model-checking and theorem-proving

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

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

Robert Kurshan, Cadence Design Systems, USA; Vladimir Levin, Bell Labs, USA; and Husnu Yenigun, Sebancy U, Turkey
Compressing transitions for model checking

Ken L. McMillan, Cadence Design Systems, USA
Applying SAT methods in unbounded symbolic model checking

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

Mitra Purandare and Fabio Somenzi, U Colorado-Boulder, USA
Vacuum cleaning CTL formulae

Sriram K. Rajamani and Jakob Rehof, Microsoft Research, USA
Conformance checking for models of asynchronous message passing software

Tatiana Rybina and Andrei Voronkov, U Manchester, UK
Using canonical representations of solutions to speed up infinite-state model checking

Ofer Strichman, Sanjit A. Seshia, and Randal E. Bryant; Carnegie Mellon U, USA
Reducing linear inequalities to propositional formulas

Aaron Stump, Clark W. Barrett, and David L. Dill; Stanford U, USA
CVC: a cooperating validity checker

Li Tan and Rance Cleaveland, State U of New York-Stony Brook, USA
Evidence-based model checking

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

Hakan L. S. Younes and Reid G. Simmons, Carnegie Mellon U, USA
Probabilistic verification of descrete event systems using acceptance sampling