| 2006 | Type-Safe Two-Level Data Transformation. | Alcino Cunha, Jos Nuno Oliveira, Joost Visser |
| 2006 | Validating the Microsoft Hypervisor. | Ernie Cohen |
| 2006 | Properties of Behavioural Model Merging. | Greg Brunet, Marsha Chechik, Sebastin Uchitel |
| 2006 | Using Domain-Independent Problems for Introducing Formal Methods. | Raymond T. Boute |
| 2006 | Automated Boundary Test Generation from JML Specifications. | Fabrice Bouquet, Frdric Dadeau, Bruno Legeard |
| 2006 | Towards Modularized Verification of Distributed Time-Triggered Systems. | Jewgenij Botaschanjan, Alexander Gruler, Alexander Harhurin, Leonid Kof, Maria Spichkova, David Trachtenherz |
| 2006 | Formal Verification of a C Compiler Front-End. | Sandrine Blazy, Zaynah Dargaye, Xavier Leroy |
| 2006 | Changing Programs Correctly: Refactoring with Specifications. | Fabian Bannwart, Peter Mller |
| 2006 | Formal Methods and Cryptography. | Michael Backes, Birgit Pfitzmann, Michael Waidner |
| 2006 | A Story About Formal Methods Adoption by a Railway Signaling Manufacturer. | Stefano Bacherini, Alessandro Fantechi, Matteo Tempestini, Niccol Zingoni |
| 2006 | Enforcer - Efficient Failure Injection. | Cyrille Artho, Armin Biere, Shinichi Honiden |
| 2006 | A Formal Template Language Enabling Metaproof. | Nuno Amlio, Susan Stepney, Fiona Polack |
| 2006 | Feature Specification and Static Analysis for Interaction Resolution. | Marc Aiguier, Karim Berkani, Pascale Le Gall |
| 2005 | A Formal Model of Addressing for Interoperating Networks. | Pamela Zave |
| 2005 | Systematic Implementation of Real-Time Models. | Martin De Wulf, Laurent Doyen, Jean-Franois Raskin |
| 2005 | Operational Semantics for Model Checking Circus. | Jim Woodcock, Ana Cavalcanti, Leonardo Freitas |
| 2005 | Timing Tolerances in Safety-Critical Software. | Alan Wassyng, Mark Lawford, Xiayong Hu |
| 2005 | Synthesis of Distributed Processes from Scenario-Based Specifications. | Jun Sun, Jin Song Dong |
| 2005 | Dynamic Component Substitutability Analysis. | Natasha Sharygina, Sagar Chaki, Edmund M. Clarke, Nishant Sinha |
| 2005 | Formally Defining and Verifying Master/Slave Speculative Parallelization. | Pierre Salverda, Grigore Rosu, Craig B. Zilles |
| 2005 | Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems. | Vlad Rusu, Herv Marchand, Thierry Jron |
| 2005 | Semantics of BPEL4WS-Like Fault and Compensation Handling. | Zongyan Qiu, Shuling Wang, Geguang Pu, Xiangpeng Zhao |
| 2005 | Model-Based Testing in Practice. | Alexander Pretschner |
| 2005 | Controlling Object Allocation Using Creation Guards. | Cees Pierik, Dave Clarke, Frank S. de Boer |
| 2005 | The Informal Nature of Systems Engineering. | Gerrit Muller |