| 2008 | Semi-external LTL Model Checking. | Stefan Edelkamp, Peter Sanders, Pavel Simecek |
| 2008 | Conflict-Tolerant Features. | Deepak D'Souza, Madhu Gopinathan |
| 2008 | The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols. | Cas J. F. Cremers |
| 2008 | Proving Conditional Termination. | Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv |
| 2008 | Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses. | Ariel Cohen, Amir Pnueli, Lenore D. Zuck |
| 2008 | Local Proofs for Linear-Time Properties of Concurrent Programs. | Ariel Cohen, Kedar S. Namjoshi |
| 2008 | Effective Program Verification for Relaxed Memory Models. | Sebastian Burckhardt, Madanlal Musuvathi |
| 2008 | The MathSAT 4SMT Solver. | Roberto Bruttomesso, Alessandro Cimatti, Anders Franzn, Alberto Griggio, Roberto Sebastiani |
| 2008 | The Barcelogic SMT Solver. | Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodrguez-Carbonell, Albert Rubio |
| 2008 | Automated Assume-Guarantee Reasoning by Abstraction Refinement. | Mihaela Gheorghiu Bobaru, Corina S. Pasareanu, Dimitra Giannakopoulou |
| 2008 | A Practical Approach to Word Level Model Checking of Industrial Netlists. | Per Bjesse |
| 2008 | CSIsat: Interpolation for LA+EUF. | Dirk Beyer, Damien Zufferey, Rupak Majumdar |
| 2008 | Thread Quantification for Concurrent Shape Analysis. | Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, Shmuel Sagiv |
| 2008 | Implied Set Closure and Its Application to Memory Consistency Verification. | Surender Baswana, Shashank K. Mehta, Vishal Powar |
| 2008 | The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis. | Michael Backes, Stefan Lorenz, Matteo Maffei, Kim Pecina |
| 2008 | Ranking Automata and Games for Prioritized Requirements. | Rajeev Alur, Aditya Kanade, Gera Weiss |
| 2008 | Monotonic Abstraction for Programs with Dynamic Memory Heaps. | Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frdric Haziza, Ahmed Rezine |
| 2007 | Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra. | Chao Wang, Zijiang Yang, Aarti Gupta, Franjo Ivancic |
| 2007 | Adaptive Symmetry Reduction. | Thomas Wahl |
| 2007 | jMoped: A Test Environment for Java Programs. | Dejvuth Suwimonteerabuth, Felix Berger, Stefan Schwoon, Javier Esparza |
| 2007 | SAT-Based Compositional Verification Using Lazy Learning. | Nishant Sinha, Edmund M. Clarke |
| 2007 | Abstraction and Counterexample-Guided Construction of | Marc Segelken |
| 2007 | A Mathematical Approach to RTL Verification. | David M. Russinoff |
| 2007 | Hybrid Systems: From Verification to Falsification. | Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi |
| 2007 | Spade: Verification of Multithreaded Dynamic and Recursive Programs. | Gal Patin, Mihaela Sighireanu, Tayssir Touili |