| 2009 | Bridging the Gap Between Model-Based Development and Model Checking. | Steven P. Miller |
| 2009 | Hierarchical Adaptive State Space Caching Based on Level Sampling. | Radu Mateescu, Anton Wijs |
| 2009 | All-Termination(T). | Panagiotis Manolios, Aaron Turon |
| 2009 | Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches. | Didier Lime, Olivier H. Roux, Charlotte Seidner, Louis-Marie Traonouez |
| 2009 | TaPAS: The Talence Presburger Arithmetic Suite. | Jrme Leroux, Grald Point |
| 2009 | Computing Weakest Strategies for Safety Games of Imperfect Information. | Wouter Kuijper, Jaco van de Pol |
| 2009 | Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications. | Hillel Kugler, Itai Segall |
| 2009 | Semantic Reduction of Thread Interleavings in Concurrent Programs. | Vineet Kahlon, Sriram Sankaranarayanan, Aarti Gupta |
| 2009 | From Tests to Proofs. | Ashutosh Gupta, Rupak Majumdar, Andrey Rybalchenko |
| 2009 | Specification Mining with Few False Positives. | Claire Le Goues, Westley Weimer |
| 2009 | RBAC-PAT: A Policy Analysis Tool for Role Based Access Control. | Mikhail I. Gofman, Ruiqi Luo, Ayla C. Solomon, Yingbin Zhang, Ping Yang, Scott D. Stoller |
| 2009 | Ground Interpolation for the Theory of Equality. | Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli |
| 2009 | Bchi Complementation and Size-Change Termination. | Seth Fogarty, Moshe Y. Vardi |
| 2009 | The Complexity of Predicting Atomicity Violations. | Azadeh Farzan, P. Madhusudan |
| 2009 | Verifying Reference Counting Implementations. | Michael Emmi, Ranjit Jhala, Eddie Kohler, Rupak Majumdar |
| 2009 | Parametric Trace Slicing and Monitoring. | Feng Chen, Grigore Rosu |
| 2009 | Learning Minimal Separating DFA's for Compositional Verification. | Yu-Fang Chen, Azadeh Farzan, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang |
| 2009 | Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. | Robert Brummayer, Armin Biere |
| 2009 | MoonWalker: Verification of .NET Programs. | Niels H. M. Aan de Brugh, Viet Yen Nguyen, Theo C. Ruys |
| 2009 | Iterating Octagons. | Marius Bozga, Codruta Grlea, Radu Iosif |
| 2009 | Path Feasibility Analysis for String-Manipulating Programs. | Nikolaj S. Bjrner, Nikolai Tillmann, Andrei Voronkov |
| 2009 | Alpaga: A Tool for Solving Parity Games with Imperfect Information. | Dietmar Berwanger, Krishnendu Chatterjee, Martin De Wulf, Laurent Doyen, Thomas A. Henzinger |
| 2009 | Compositional Predicate Abstraction from Game Semantics. | Adam Bakewell, Dan R. Ghica |
| 2009 | Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads. | Mohamed Faouzi Atig, Ahmed Bouajjani, Shaz Qadeer |
| 2008 | Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking. | Martin De Wulf, Laurent Doyen, Nicolas Maquet, Jean-Franois Raskin |