| 2008 | BACH : Bounded ReAchability CHecker for Linear Hybrid Automata. | Lei Bu, You Li, Linzhang Wang, Xuandong Li |
| 2008 | A Refinement Approach to Design and Verification of On-Chip Communication Protocols. | Peter Bhm, Tom Melham |
| 2008 | A Write-Based Solver for SAT Modulo the Theory of Arrays. | Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodrguez-Carbonell, Albert Rubio |
| 2008 | Word-Level Sequential Memory Abstraction for Model Checking. | Per Bjesse |
| 2008 | Automatic Non-Interference Lemmas for Parameterized Model Checking. | Jesse D. Bingham |
| 2008 | Consistency Checking of All Different Constraints over Bit-Vectors within a SAT Solver. | Armin Biere, Robert Brummayer |
| 2008 | Optimal Constraint-Preserving Netlist Simplification. | Jason Baumgartner, Hari Mony, Adnan Aziz |
| 2007 | Global Optimization of Compositional Systems. | Fadi A. Zaraket, John Pape, Adnan Aziz, Margarida F. Jacome, Sarfraz Khurshid |
| 2007 | Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS Designs. | Mohamed H. Zaki, Ghiath Al Sammane, Sofine Tahar, Guy Bois |
| 2007 | Circuit Level Verification of a High-Speed Toggle. | Chao Yan, Mark R. Greenstreet |
| 2007 | Induction in CEGAR for Detecting Counterexamples. | Chao Wang, Aarti Gupta, Franjo Ivancic |
| 2007 | A Logic for GSTE. | Edward Smith |
| 2007 | Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC. | Jocelyn Simmonds, Jessica Davies, Arie Gurfinkel, Marsha Chechik |
| 2007 | Formal Verification of Partial Good Self-Test Fencing Structures. | Adrian E. Seigler, Gary A. Van Huben, Hari Mony |
| 2007 | A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware. | Julien Schmaltz |
| 2007 | Improved Design Debugging Using Maximum Satisfiability. | Sean Safarpour, Hratch Mangassarian, Andreas G. Veneris, Mark H. Liffiton, Karem A. Sakallah |
| 2007 | Analyzing Gene Relationships for Down Syndrome with Labeled Transition Graphs. | Neha Rungta, Hyrum Carroll, Eric G. Mercer, Randall J. Roper, Mark J. Clement, Quinn Snell |
| 2007 | A Mechanized Refinement Framework for Analysis of Custom Memories. | Sandip Ray, Jayanta Bhadra |
| 2007 | Modeling Time-Triggered Protocols and Verifying Their Real-Time Schedules. | Lee Pike |
| 2007 | A Quantitative Completeness Analysis for Property-Sets. | Martin Oberknig, Martin Schickel, Hans Eveking |
| 2007 | Automating Hazard Checking in Transaction-Level Microarchitecture Models. | Yogesh S. Mahajan, Sharad Malik |
| 2007 | What Triggers a Behavior? | Orna Kupferman, Yoad Lustig |
| 2007 | Lifting Propositional Interpolants to the Word-Level. | Daniel Kroening, Georg Weissenbacher |
| 2007 | Industrial Strength SAT-based Alignability Algorithm for Hardware Equivalence Verification. | Daher Kaiss, Marcelo Skaba, Ziyad Hanna, Zurab Khasidashvili |
| 2007 | Boosting Verification by Automatic Tuning of Decision Procedures. | Frank Hutter, Domagoj Babic, Holger H. Hoos, Alan J. Hu |