Regular Papers

Tilman Gloekler, Jason Baumgartner, Devi Shanmugam, Rick Seigler, Gary Van Huben, Barinjato Ramanandray, Hari Mony, and Paul Roessler.
Enabling Large-Scale Pervasive Logic Verification through Multi-Algorithmic Formal Reasoning.

Sava Krstic, Jordi Cortadella, Mike Kishinevsky, and John O'Leary.
Synchronous Elastic Networks.

Ashish Darbari.
Symmetry reduction for STE model checking.

Shiva Nejati, Mihaela Gheorghiu, and Marsha Chechik.
Thorough Checking Revisited.

Barbara Jobstmann and Roderick Bloem.
Optimizations for LTL Synthesis.

Zurab Khasidashvili, Marcelo Skaba, Daher Kaiss, and Ziyad Hanna.
Post-reboot Equivalence and Compositional Verification of Hardware.

Byron Cook, Daniel Kroening, and Natasha Sharygina.
Over-Approximating Boolean Programs with Unbounded Thread Creation.

Claude Helmstetter, Florence Maraninchi, Laurent Maillet-Contoz, and Matthieu Moy.
Automatic Generation of Schedulings for Improving the Test Coverage of Systems-on-a-Chip.

Amir Hossein Ghamarian, Marc Geilen, Twan Basten, Bart Theelen, Mohammad Reza Mousavi, and Sander Stuijk.
Liveness and Boundedness of Synchronous Data Flow Graphs.

Alessandro Cimatti, Marco Roveri, Simone Semprini, and Stefano Tonetta.
From PSL to NBA: A Modular Symbolic Encoding.

Florian Pigorsch, Christoph Scholl, and Stefan Disch.
Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, And Quantifier Scheduling.

Xiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, and Ching-Tsun Chou.
Reducing Verification Complexity of a Multicore Coherence Protocol Using Assume/Guarantee.

Husam Abu-Haimed, David Dill, and Sergey Berezin.
A Refinement Method for Validity Checking of Quantified First-Order Formulas in Hardware Verification.

Hyondeuk Kim and Fabio Somenzi.
Finite Instantiations for Integer Difference Logic.

Jun Sawada and Erik Reeber.
ACL2SIX : A Hint used to Integrate a Theorem Prover and an Automated Verification Tool.

Namrata Shekhar, Priyank Kalla, M. Brandon Meredith, and Florian Enescu.
Simulation Bounds for Equivalence Verification of Arithmetic Datapaths with Finite Word-Length Operands.

Neha Rungta and Eric Mercer.
An Improved Distance Heuristic Function for Directed Software Model Checking.

Sagar Chaki and Nishant Sinha.
Assume-Guarantee Reasoning for Deadlock.

Eric Gregoire, Bertrand Mazure, and Cedric Piette.
Tracking MUSes and Strict Inconsistent Covers.

Michael Gordon, Warren Hunt, Matt Kaufmann, and James Reynolds.
An Integration of HOL and ACL2.

Short Papers

Cameron Brien and Sharad Malik.
Understanding the Dynamic Behaviour of Modern DPLL SAT Solvers through Visual Analysis.

Johannes Faber and Roland Meyer.
Model Checking Data-Dependent Real-Time Properties of the European Train Control System.

Abu Nasser Mohammed Abdullah, Behzad Akbarpour, and Sofiene Tahar.
Formal Analysis and Verification of an OFDM Modem Design using HOL.

Ali Habibi, Haja Moinudeen, and Sofiene Tahar.
Design for Verification of the PCI-X Bus.

Hossein Sheini and Karem Sakallah.
Ario: A Linear Integer Arithmetic Logic Solver.

Julien Schmaltz.
A Formal Model of Lower System Layers.