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

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