| 2007 | Parametric and Sliced Causality. | Feng Chen, Grigore Rosu |
| 2007 | Hector: Software Model Checking with Cooperating Analysis Plugins. | Nathaniel Charlton, Michael Huth |
| 2007 | Verification Across Intellectual Property Boundaries. | Sagar Chaki, Christian Schallhart, Helmut Veith |
| 2007 | A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems. | Roberto Bruttomesso, Alessandro Cimatti, Anders Franzn, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani |
| 2007 | C32SAT: Checking C Expressions. | Robert Brummayer, Armin Biere |
| 2007 | Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures. | Ahmed Bouajjani, Sverine Fratani, Shaz Qadeer |
| 2007 | Revamping TVLA: Making Parametric Shape Analysis Competitive. | Igor Bogudlov, Tal Lev-Ami, Thomas W. Reps, Mooly Sagiv |
| 2007 | RAT: A Tool for the Formal Analysis of Requirements. | Roderick Bloem, Roberto Cavada, Ingo Pill, Marco Roveri, Andrei Tchaltsev |
| 2007 | Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. | Dirk Beyer, Thomas A. Henzinger, Grgory Thoduloz |
| 2007 | Algorithms for Interface Synthesis. | Dirk Beyer, Thomas A. Henzinger, Vasu Singh |
| 2007 | Shape Analysis for Composite Data Structures. | Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang |
| 2007 | UPPAAL-Tiga: Time for Playing Games! | Gerd Behrmann, Agns Cougnard, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, Didier Lime |
| 2007 | LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals. | Bernd Becker, Christian Dax, Jochen Eisinger, Felix Klaedtke |
| 2007 | CVC3. | Clark W. Barrett, Cesare Tinelli |
| 2007 | I/O Efficient Accepting Cycle Detection. | Jiri Barnat, Lubos Brim, Pavel Simecek |
| 2007 | Leaping Loops in the Presence of Abstraction. | Thomas Ball, Orna Kupferman, Mooly Sagiv |
| 2007 | Structural Abstraction of Software Verification Conditions. | Domagoj Babic, Alan J. Hu |
| 2007 | Comparison Under Abstraction for Verifying Linearizability. | Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, Eran Yahav |
| 2007 | Magnifying-Lens Abstraction for Markov Decision Processes. | Luca de Alfaro, Pritam Roy |
| 2007 | An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games. | Luca de Alfaro, Marco Faella |
| 2007 | Parameterized Verification of Infinite-State Processes with Global Conditions. | Parosh Aziz Abdulla, Giorgio Delzanno, Ahmed Rezine |
| 2006 | Antichains: A New Algorithm for Checking Universality of Finite Automata. | Martin De Wulf, Laurent Doyen, Thomas A. Henzinger, Jean-Franois Raskin |
| 2006 | LEVER: A Tool for Learning Based Verification. | Abhay Vardhan, Mahesh Viswanathan |
| 2006 | Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation. | Rachel Tzoref, Orna Grumberg |
| 2006 | cascade: C Assertion Checker and Deductive Engine. | Nikhil Sethi, Clark W. Barrett |