Accepted Papers

Akash Lal, Thomas Reps
Improving Pushdown System Model Checking

Keijo Heljanko, Tommi Junttila, Misa Keinänen, Martin Lange, and Timo Latvala
Bounded Model Checking for Weak Alternating Buchi Automata

Dirk Beyer, Tom Henzinger, and Grégory Théoduloz
Lazy Shape Analysis

Jan-Willem Roorda, Koen Claessen
SAT-based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation

Jochen Klose, Tobe Toben, Bernd Westphal, and Hartmut Wittke
Check It Out: On the Efficient Formal Verification of Live Sequence Charts

Sébastien Bardin, Jerome Leroux, and Gérald Point
FAST Extended Release

Robert Colvin, Lindsay Groves, Victor Luchangco, and Mark Moir
Formal Verification of a Lazy Concurrent List-Based Set

Amitabha Roy, Chuck Fleckenstein, Stephan Zeisset, and John Huang
Fast and Generalized Polynomial Time Memory Consistency Verification

Himanshu Jain, Franjo Ivancic, Aarti Gupta, Ilya Shlyakhter, and Chao Wang
Using Statically Computed Invariants inside the Predicate Abstraction and Refinement Loop

Bernard Boigelot, Frédéric Herbreteau
The Power of Hybrid Acceleration

Josh Berdine, Byron Cook, Dino Distefano, and Peter O'Hearn
Automatic termination proofs for programs with shape-shifting heaps

Byron Cook, Andreas Podelski, and Andrey Rybalchenko
Terminator: Beyond Safety

Koushik Sen, Mahesh Viswanathan
Model Checking Multithreaded Programs with Asynchronous Atomic Methods

Grigore Rosu, Saddek Bensalem
Allen Linear (Interval) Temporal Logic -- Translation to LTL and Monitor Synthesis

Kenneth Roe
The Heuristic Theorem Prover: Yet another SMT Modulo Theorem Prover

Denis Gopan, Thomas Reps
Lookahead Widening

Azadeh Farzan, P. Madhusudan
Causal Atomicity

Bruno Dutertre, Leonardo de Moura
A Fast Linear-Arithmetic Solver for DPLL(T)

Flavio M. de Paula, Alan Hu
EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation

Sebastian Burckhardt, Rajeev Alur, and Milo M.K. Martin
Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study

Daniel Kroening, Georg Weissenbacher
Counterexamples with Loops for Predicate Abstraction

Radu Iosif, Marius Bozga, Ahmed Bouajjani, Peter Habermehl, Pierre Moro, and Tomas Vojnar
Programs with Lists are Counter Automata

Doron Bustan, John Havlicek
Some complexity results for SystemVerilog Assertions

Pavel Krcal, Wang Yi
Communicating Timed Automata: The More Synchronous, the More Difficult to Verify

Luca de Alfaro, Marco Faella, B. Thomas Adler, Leandro Dias Da Silva, Axel Legay, Vishwanath Raman, and Pritam Roy
Ticc: A Tool for Interface Compatibility and Composition

Mark Braverman
Termination of Integer Linear Programs

Abhay Vardhan, Mahesh Viswanathan
LEVER: A tool for Learning Based Verification

Vineet Kahlon, Aarti Gupta, and Nishant Sinha
Symbolic Model Checking of Concurrent Programs using Partial Orders and On-the-fly Transactions

Arie Gurfinkel, Ou Wei, and marsha chechik
Yasm: A Software Model-Checker for Verification and Refutation

Rachel Tzoref, Orna Grumberg
Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation

Rajeev Alur, Swarat Chaudhuri, and P. Madhusudan
Languages of Nested Trees

Kenneth McMillan
Lazy Abstraction with Interpolants

Marta Kwiatkowska, Gethin Norman, and David Parker
Symmetry Reduction for Probabilistic Model Checking

Andreas Griesmayer, Roderick Bloem, and Byron Cook
Repair of Boolean Programs with an Application to C

Orna Kupferman, Moshe Y. Vardi, and Nir Piterman
Safraless Compositional Synthesis

Nikhil Sethi, Clark Barrett
Cascade: C Assertion Checker and Deductive Engine

Jochen Eisinger, Felix Klaedtke
Don't Care Words with Application to the Automata-based Approach for Real Addition

Martin De Wulf, Laurent Doyen, Tom Henzinger, and Jean-Francois Raskin
Antichains: A New Algorithm for Checking Universality of Finite Automata

Jiri Barnat, Lubos Brim, Ivana Cerna, Pavel Moravec, Petr Rockai, and Pavel Simecek
DiVinE - A Tool for Distributed Verification

Tal Lev-Ami, Neil Immerman, and Mooly Sagiv
Abstraction for Shape Analysis with Fast and Precise Transformers

Sudeep Juvekar, Nir Piterman
Minimizing Generalized Buchi Automata

Panagiotis Manolios, Daron Vroon
Termination Analysis with Calling Context Graphs

Koushik Sen, Gul Agha
CUTE and jCUTE : Concolic Unit Testing and Explicit Path Model-Checking Tools

Shuvendu Lahiri, Robert Nieuwenhuis, and Albert Oliveras
SMT Techniques for Predicate Abstraction

Roman Gershman, Maya Koifman, and Ofer Strichman
Deriving small unsatisfiable cores with dominators