| 2010 | The Static Driver Verifier Research Platform. | Thomas Ball, Ella Bounimova, Vladimir Levin, Rahul Kumar, Jakob Lichtenberg |
| 2010 | Fences in Weak Memory Models. | Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell |
| 2010 | Abstract Analysis of Symbolic Executions. | Aws Albarghouthi, Arie Gurfinkel, Ou Wei, Marsha Chechik |
| 2010 | Simulation Subsumption in Ramsey-Based Bchi Automata Universality and Inclusion Testing. | Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Luks Holk, Chih-Duo Hong, Richard Mayr, Toms Vojnar |
| 2009 | A Concurrent Portfolio Approach to SMT Solving. | Christoph M. Wintersteiger, Youssef Hamadi, Leonardo Mendona de Moura |
| 2009 | Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences. | Sven Verdoolaege, Gerda Janssens, Maurice Bruynooghe |
| 2009 | Reducing Context-Bounded Concurrent Reachability to Sequential Reachability. | Salvatore La Torre, P. Madhusudan, Gennaro Parlato |
| 2009 | PAT: Towards Flexible Verification under Fairness. | Jun Sun, Yang Liu, Jin Song Dong, Jun Pang |
| 2009 | Regression Verification: Proving the Equivalence of Similar Programs. | Ofer Strichman |
| 2009 | VS3: SMT Solvers for Program Verification. | Saurabh Srivastava, Sumit Gulwani, Jeffrey S. Foster |
| 2009 | Component-Based Construction of Real-Time Systems in BIP. | Joseph Sifakis |
| 2009 | Translation Validation: From Simulink to C. | Michael Ryabtsev, Ofer Strichman |
| 2009 | Cardinality Abstraction for Declarative Networking Applications. | Juan Antonio Navarro Prez, Andrey Rybalchenko, Atul Singh |
| 2009 | TASS: Timing Analyzer of Scenario-Based Specifications. | Minxue Pan, Lei Bu, Xuandong Li |
| 2009 | On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure. | David Monniaux |
| 2009 | Generalizing DPLL to Richer Logics. | Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv |
| 2009 | Reducing Test Inputs Using Information Partitions. | Rupak Majumdar, Ru-Gang Xu |
| 2009 | MCMAS: A Model Checker for the Verification of Multi-Agent Systems. | Alessio Lomuscio, Hongyang Qu, Franco Raimondi |
| 2009 | Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints. | Peter Lammich, Markus Mller-Olm, Alexander Wenner |
| 2009 | Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers. | Shuvendu K. Lahiri, Shaz Qadeer, Zvonimir Rakamaric |
| 2009 | Intra-module Inference. | Shuvendu K. Lahiri, Shaz Qadeer, Juan P. Galeotti, Jan W. Voung, Thomas Wies |
| 2009 | Modelling Epigenetic Information Maintenance: A Kappa Tutorial. | Jean Krivine, Vincent Danos, Arndt Benecke |
| 2009 | A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints. | Nathan Kitchen, Andreas Kuehlmann |
| 2009 | Mixed-Signal System Verification: A High-Speed Link Example. | Jaeha Kim |
| 2009 | Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models. | Aditya Kanade, Rajeev Alur, Franjo Ivancic, S. Ramesh, Sriram Sankaranarayanan, K. C. Shashidhar |