| 2006 | Lookahead Widening. | Denis Gopan, Thomas W. Reps |
| 2006 | Deriving Small Unsatisfiable Cores with Dominators. | Roman Gershman, Maya Koifman, Ofer Strichman |
| 2006 | Causal Atomicity. | Azadeh Farzan, P. Madhusudan |
| 2006 | Don't Care Words with an Application to the Automata-Based Approach for Real Addition. | Jochen Eisinger, Felix Klaedtke |
| 2006 | A Fast Linear-Arithmetic Solver for DPLL(T). | Bruno Dutertre, Leonardo Mendona de Moura |
| 2006 | I Think I Voted: E-Voting vs. Democracy. | David L. Dill |
| 2006 | Formal Specifications on Industrial-Strength Code-From Myth to Reality. | Manuvir Das |
| 2006 | Terminator: Beyond Safety. | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
| 2006 | Formal Verification of a Lazy Concurrent List-Based Set Algorithm. | Robert Colvin, Lindsay Groves, Victor Luchangco, Mark Moir |
| 2006 | Some Complexity Results for SystemVerilog Assertions. | Doron Bustan, John Havlicek |
| 2006 | Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study. | Sebastian Burckhardt, Rajeev Alur, Milo M. K. Martin |
| 2006 | Termination of Integer Linear Programs. | Mark Braverman |
| 2006 | Programs with Lists Are Counter Automata. | Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Toms Vojnar |
| 2006 | The Power of Hybrid Acceleration. | Bernard Boigelot, Frdric Herbreteau |
| 2006 | Lazy Shape Analysis. | Dirk Beyer, Thomas A. Henzinger, Grgory Thoduloz |
| 2006 | Automatic Termination Proofs for Programs with Shape-Shifting Heaps. | Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn |
| 2006 | DiVinE - A Tool for Distributed Verification. | Jiri Barnat, Lubos Brim, Ivana Cern, Pavel Moravec, Petr Rockai, Pavel Simecek |
| 2006 | FAST Extended Release. | Sbastien Bardin, Jrme Leroux, Grald Point |
| 2006 | Languages of Nested Trees. | Rajeev Alur, Swarat Chaudhuri, P. Madhusudan |
| 2006 | Ticc: A Tool for Interface Compatibility and Composition. | B. Thomas Adler, Luca de Alfaro, Leandro Dias da Silva, Marco Faella, Axel Legay, Vishwanath Raman, Pritam Roy |
| 2005 | Ymer: A Statistical Model Checker. | Hkan L. S. Younes |
| 2005 | Probabilistic Verification for "Black-Box" Systems. | Hkan L. S. Younes |
| 2005 | Action Language Verifier, Extended. | Tuba Yavuz-Kahveci, Constantinos Bartzis, Tevfik Bultan |
| 2005 | Saturn: A SAT-Based Tool for Bug Detection. | Yichen Xie, Alex Aiken |
| 2005 | Syntax-Driven Reachable State Space Construction of Synchronous Reactive Programs. | Eric Vecchi, Robert de Simone |