Regular Papers
A Refinement Approach to Design and Verification of On-Chip Communication ProtocolsPeter Boehm and Tom Melham.
A Temporal Language for SystemC
Deian Tabakov and Moshe Vardi.
A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance
Orna Kupferman, Wenchao Li and Sanjit A. Seshia.
A Theory-Based Decision Heuristic for DPLL(T)
Dan Goldwasser, Ofer Strichman and Shai Fine.
A Write-Based Solver for SAT Modulo the Theory of Arrays
Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez Carbonell and Albert Rubio.
Augmenting a Regular Expression-Based Temporal Logic with Local Variables
Cindy Eisner and Dana Fisman.
Automatic Formal Verification of Block Cipher Implementations
Eric Smith and David Dill.
Automatic Generation of Local Repairs for Boolean Programs
Roopsha Samanta, Jyotirmoy Deshmukh and E Allen Emerson.
Automatic Non-interference Lemmas for Parameterized Model Checking
Jesse Bingham.
BackSpace: Formal Analysis for Post-Silicon Debug
Flavio M. de Paula, Marcel Gort, Alan Hu, Steve Wilton and Jin Yang.
Beyond Vacuity: Towards the Strongest Passing Formula
Hana Chockler, Arie Gurfinkel and Ofer Strichman.
Combining Predicate and Numeric Abstraction for Software Model Checking
Arie Gurfinkel and Sagar Chaki.
Going with the Flow: Parameterized Verification using Message Flows
Murali Talupur and Mark Tuttle.
Invariant-Strengthened Elimination of Dependent State Elements
Michael Case, Alan Mishchenko, Robert Brayton, Jason Baumgartner and Hari Mony.
Machine-code verification for multiple architectures - An application of decompilation into logic
Magnus O. Myreen, Konrad Slind and Mike Gordon.
Model Checking Nash Equilibria in MAD Distributed Systems
Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci, Lorenzo Alvisi, Allen Clement and Harry Li.
Optimal Constraint-Preserving Netlist Simplification
Jason Baumgartner, Hari Mony and Adnan Aziz.
Recording Synthesis History for Sequential Verification
Alan Mishchenko and Robert Brayton.
Scaling up the formal verification of Lustre programs with SMT-based techniques
George Hagen and Cesare Tinelli.
Scheduling optimisations for SPIN to minimise buffer requirements in synchronous data flow
Pieter Hartel and Theo Ruys.
Symbolic Program Analysis using Term Rewriting and Generalization
Nishant Sinha.
Trading off SAT search and Variable Quantifications for effective Unbounded Model Checking
Gianpiero Cabodi, Paolo Camurati, Marco Murciano, Luz Garcia, Sergio Nocco and Stefano Quer.
Verifying an Arbiter Circuit
Chao Yan and Mark Greenstreet.
Word-Level Sequential Memory Abstraction for Model Checking
Per Bjesse.
Short Papers
BACH : Bounded Reachability Checker for Linear Hybrid AutomataLei Bu, You Li, Linzhang Wang and Xuandong Li.
Consistency Checking of All Different Constraints over Bit-Vectors within a SAT Solver
Armin Biere and Robert Brummayer.
Formal Verification of Hardware Support For Advanced Encryption Standard
Anna Slobodova.
Mechanized Information Flow Analysis through Inductive Assertions
Warren Hunt, Robert Krug, Sandip Ray and Bill Young.