Regular PapersA Refinement Approach to Design and Verification of On-Chip Communication Protocols
Peter 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.
Automatic Formal Verification of Block Cipher Implementations
Eric Smith and David Dill.
Automatic Non-interference Lemmas for Parameterized Model Checking
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.
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
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.
Word-Level Sequential Memory Abstraction for Model Checking
Short PapersBACH : Bounded Reachability Checker for Linear Hybrid Automata
Lei Bu, You Li, Linzhang Wang and Xuandong Li.
Formal Verification of Hardware Support For Advanced Encryption Standard