Regular Papers

Sara Adams , Magnus Bjork, Tom Melham, and Carl Seger.
Automatic Abstraction in Symbolic Trajectory Evaluation

Daher Kaiss, Marcelo Skaba, Ziyad Hanna, and Zurab Khasidashvili.
Industrial Strength SAT-based Alignability Algorithm for Hardware Equivalence Verification

Michael Case, Alan Mishchenko, and Robert Brayton.
Automated Extraction of Inductive Invariants to Aid Model Checking

Jocelyn Simmonds, Jessica Davies, Arie Gurfinkel, and Marsha Chechik.
Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC

Xiaofang Chen, Steven German, and Ganesh Gopalakrishnan .
Transaction Based Modeling and Verification of Hardware Protocol Implementations

Aaron Hurst, Alan Mishchenko, and Robert Brayton.
Fast Minimum Register Retiming Via Binary Maximum-Flow

Fadi Zaraket, John Pape, Margarida Jacome, Adnan Aziz, and Sarfraz Khurshid.
COSE: a Technique for Co-optimizing Embedded Systems

Orna Kupferman and Yoad Lustig.
What triggers a behavior?

Julien Schmaltz.
A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware

Yan Chen, Yujing He, Fei Xie, and Jin Yang.
Automatic Abstraction Refinement for Generalized Symbolic Trajectory Evaluation

Koen Claessen.
A Coverage Analysis for Safety Property Lists

Edward Smith.
A Logic for GSTE

Hana Chockler, Benny Godlin, Eitan Farchi, and Sergey Novikov.
Cross-Entropy Based Testing

Chao Wang , Aarti Gupta, and Franjo Ivancic.
Induction in CEGAR for Detecting Counterexamples

Sean Safarpour, Mark Liffiton, Hratch Mangassarian, Andreas Veneris, and Karem Sakallah.
Improved Design Debugging using Maximum Satisfiability

Roberto Cavada, Alessandro Cimatti, Anders Franzen, Kalyanasundaram Krishnamani, Marco Roveri, and R.K. Shyamasundar.
Computing Abstractions by integrating BDDs and SMT Solvers

Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, and Richard Trefler.
Algorithmic Analysis of Piecewise FIFO Systems

Chao Yan and Mark Greenstreet.
Circuit-Level Verification of a High-Speed Toggle

Aaron Bradley and Zohar Manna.
Safety Checking through Invariant Generation of Clauses

Frank Hutter, Domagoj Babic, Holger Hoos, and Alan Hu.
Boosting Verification by Automatic Tuning of Decision Procedures

Ariel Cohen, John O'Leary, Amir Pnueli, Mark R. Tuttle, and Lenore Zuck.
Verifying Correctness of Transactional Memories

Mohamed Zaki, Ghiath Al Sammane, Sofiene Tahar, and Guy Bois.
Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS Designs

Short Papers

Sandip Ray and Jayanta Bhadra.
A Mechanized Refinement Framework for Analysis of Custom Memories

Kathi Fisler.
Two-Dimensional Regular Expressions for Compositional Bus Protocols

Alon Flaisher, Alon Gluska, and Eli Singerman.
Case study: Integrating FV and DV within the Verification of Intel(r) Core(TM)2 Microprocessor

Martin Oberkönig, Martin Schickel, and Hans Eveking.
A Quantitative Completeness Analysis for Property-Sets

Yogesh Mahajan and Sharad Malik.
Automating Hazard Checking in Transaction-Level Microarchitecture Models

Adrian Seigler, Gary Van Huben, and Hari Mony.
Formal Verification of Partial Good Self-Test Fencing Structures

Neha Rungta, Hyrum Carroll, Eric Mercer, Randall Roper, Mark Clement, and Quinn Snell.
Analyzing Gene Relationships for Down Syndrome with Labeled Transitions Graphs