| 2009 | Logahedra: A New Weakly Relational Domain. | Jacob M. Howe, Andy King |
| 2009 | Memory Usage Verification Using Hip/Sleek. | Guanhua He, Shengchao Qin, Chenguang Luo, Wei-Ngan Chin |
| 2009 | 3-Valued Abstraction for (Bounded) Model Checking. | Orna Grumberg |
| 2009 | Verifying VLSI Circuits. | Mark R. Greenstreet |
| 2009 | Exploring the Scope for Partial Order Reduction. | Jaco Geldenhuys, Henri Hansen, Antti Valmari |
| 2009 | Solving Parity Games in Practice. | Oliver Friedmann, Martin Lange |
| 2009 | CLAN: A Tool for Contract Analysis and Conflict Discovery. | Stephen Fenech, Gordon J. Pace, Gerardo Schneider |
| 2009 | Incremental False Path Elimination for Static Software Analysis. | Ansgar Fehnker, Ralf Huuck, Sean Seefried |
| 2009 | On-the-fly Emptiness Check of Transition-Based Streett Automata. | Alexandre Duret-Lutz, Denis Poitrenaud, Jean-Michel Couvreur |
| 2009 | Synthesis of Fault-Tolerant Distributed Systems. | Rayna Dimitrova, Bernd Finkbeiner |
| 2009 | Specification Languages for Stutter-Invariant Regular Properties. | Christian Dax, Felix Klaedtke, Stefan Leue |
| 2009 | A Data Symmetry Reduction Technique for Temporal-epistemic Logic. | Mika Cohen, Mads Dam, Alessio Lomuscio, Hongyang Qu |
| 2009 | LTL Model Checking of Time-Inhomogeneous Markov Chains. | Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre |
| 2009 | Dynamic Observers for the Synthesis of Opaque Systems. | Franck Cassez, Jrmy Dubreil, Herv Marchand |
| 2009 | Untitled record | Alarico Campetelli, Alexander Gruler, Martin Leucker, Daniel Thoma |
| 2009 | TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets. | Joakim Byg, Kenneth Yrke Jrgensen, Jir Srba |
| 2009 | Quantitative Analysis under Fairness Constraints. | Christel Baier, Marcus Grer, Frank Ciesinski |
| 2009 | Automated Analysis of Data-Dependent Programs with Dynamic Memory. | Parosh Aziz Abdulla, Muhsin Atto, Jonathan Cederberg, Ran Ji |
| 2008 | Alaska. | Martin De Wulf, Laurent Doyen, Nicolas Maquet, Jean-Franois Raskin |
| 2008 | Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions. | Chao Wang, Yu Yang, Aarti Gupta, Ganesh Gopalakrishnan |
| 2008 | Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions. | Farn Wang |
| 2008 | Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic. | Hiroaki Shimizu, Kiyoharu Hamaguchi, Toshinobu Kashiwabara |
| 2008 | Trust and Automation in Verification Tools. | Natarajan Shankar |
| 2008 | Tests, Proofs and Refinements. | Sriram K. Rajamani |
| 2008 | Computation Tree Regular Logic for Genetic Regulatory Networks. | Radu Mateescu, Pedro T. Monteiro, Estelle Dumas, Hidde de Jong |