CAV 2007

Computer Aided Verification (CAV)

19th International Conference

July 3-7, 2007, Berlin, Germany


Accepted Papers

Regular Papers

Nishant Sinha and Edmund Clarke. SAT-based Compositional Verification using 
Lazy Learning
Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O'Hearn, 
Thomas Wies and Hongseok Yang. Shape analysis for composite data structures
Marc Segelken. Abstraction and Counterexample-guided Construction of 
Omega-automata for Model Checking of Step-discrete linear Hybrid Models
Jonathan Ezekiel, Gerald Lüttgen and Gianfranco Ciardo. Parallelising Symbolic 
State-Space Generators
Jiri Barnat, Lubos Brim and Pavel Simecek. I/O Efficient Accepting Cycle 
Detection
Vineet Kahlon, Yu Yang, Sriram Sankaranarayanan and Aarti Gupta. Fast and 
Accurate Static Data Race Detection for Concurrent Programs
Ariel Cohen and Kedar Namjoshi. Local Proofs for Global Safety Properties
Feng Chen and Grigore Rosu. Parametric and Sliced Causality
Thomas Ball, Orna Kupferman and Mooly Sagiv. Leaping Loops in the Presence of 
Abstraction
Chao Wang, Zijiang Yang, Aarti Gupta and Franjo Ivancic. Using Counterexamples 
for Improving the Precision of Reachability Computation with Polyhedra
Tarik Nahhal and Thao Dang. Test Coverage for Continuous and Hybrid Systems
Oded Maler, Dejan Nickovic and Amir Pnueli. On Synthesizing Controllers  from 
Bounded-Response Properties
Ofer Strichman and Arie Matsliah. Underapproximation for Model-Checking Based 
on Random Cryptographic Constructions
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
Domagoj Babic and Alan Hu. Structural Abstraction of Software Verification 
Conditions
Sumit Gulwani and Ashish Tiwari. An Abstract Domain
for Analyzing Heap-Manipulating Low-Level Software
Daphna Amit, Noam Rinetzky, Thomas Reps, Mooly Sagiv and Eran Yahav. 
Comparison under Abstraction for Verifying Linearizability
Ahmed Bouajjani, Severine Fratani and Shaz Qadeer. Bounded Context Switch 
Analysis of Multithreaded Programs with Dynamic Linked Structures.
Mayank Saksena and Bengt Jonsson. Systematic Acceleration in Regular Model
Checking
Joost-Pieter Katoen, Martin Leucker, Daniel Klink and Verena Wolf. 
Three-Valued Abstraction for Continuous-Time Markov Chains
Alessandro Cimatti, Marco Roveri, Viktor Schuppan and Stefano Tonetta. Boolean 
Abstraction for Temporal Logic Satisfiability
Erion Plaku, Moshe Vardi and Lydia Kavraki. Hybrid Systems: From Verification 
to Falsification
Sagar Chaki, Christian Schallhart and Helmut Veith. Verification Across 
Intellectual Property Boundaries
Ahmed Rezine, Parosh Abdulla and Giorgio Delzanno. Parameterized Verification 
of Infinite-state Processes with Global Conditions
Luca de Alfaro and Marco Faella. Accelerated Algorithms for 3-Color Parity 
Games with an Application to Timed Games
Denis Gopan and Thomas Reps. Low-Level Library Analysis and Summarization
Orna Kupferman, Nir Piterman and Moshe Vardi. From Liveness to Promptness
Pritam Roy and Luca de Alfaro. Magnifying-Lens Abstraction for Markov Decision 
Processes
Vijay Ganesh and David Dill. A Decision Procedure for Bit-Vectors and Arrays
Ranjit Jhala and Ken McMillan. Array Abstractions from Proofs
Dirk Beyer, Thomas A. Henzinger and Grégory Théoduloz.
Configurable Software Verification: Concretizing the Convergence
of Model Checking and Program Analysis
Thomas Wahl. Adaptive Symmetry Reduction
Anubhav Gupta, Ken McMillan and Zhaohui Fu. Automated Assumption Generation 
for Compositional Verification


Tool Presentations

Gael Patin, Mihaela Sighireanu and Tayssir Touili. SPADE: Verification of 
Multithreaded  Dynamic and Recursive Programs
Jean-Christophe Filliatre and Claude Marché. The Why/Krakatoa/Caduceus 
Platform for Deductive Program Verification
Hubert Garavel, Radu Mateescu, Frédéric Lang and Wendelin Serwe. CADP 2006: A 
Toolbox for the Construction and Analysis of Distributed Processes
Robert Brummayer and Armin Biere. C32SAT: Checking C Expressions
Barbara Jobstmann, Stefan Galler, Martin Weiglhofer and Roderick Bloem. Anzu: A Tool for 
Property Synthesis
Roderick Bloem, Roberto Cavada, Ingo Pill, Marco Roveri and Andrei Tchaltsev. 
RAT: A Tool for the Formal Analysis of Requirements
Bernd Becker, Christian Dax, Jochen Eisinger and Felix Klaedtke. LIRA: 
Handling Constraints of Linear Arithmetics over the Integers and the Reals
Nathaniel Charlton and Michael Huth. Hector: software model checking with 
cooperating analysis plugins
Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim G. Larsen 
and Didier Lime. Uppaal-Tiga: Time for Playing Games!
Igor Bogudlov, Tal Lev-Ami, Thomas Reps and Mooly Sagiv.
Revamping TVLA: Making Parametric Shape Analysis Competitive
Martin Ouimet and Kristina Lundqvist. The TASM Toolset: Specification, 
Simulation, and Formal Verification of Real-Time Systems

Panagiotis Manolios, Daron Vroon and Sudarshan Srinivasan. BAT: The Bit-Level 
Analysis Tool
Dejvuth Suwimonteerabuth, Felix Berger, Stefan Schwoon and Javier Esparza. 
jMoped: A Test Environment for Java programs
Clark Barrett and Cesare Tinelli. CVC3