| 2005 | Modular Verification of Static Class Invariants. | K. Rustan M. Leino, Peter Mller |
| 2005 | An Approach to Unfolding Asynchronous Communication Protocols. | Yu Lei, S. Purushothaman Iyer |
| 2005 | An MDA Approach Towards Integrating Formal and Informal Modeling Languages. | Soon-Kyeong Kim, Damian Burger, David A. Carrington |
| 2005 | Verifying Scenario-Based Aspect Specifications. | Emilia Katz, Shmuel Katz |
| 2005 | Decoupling in Object Orientation. | Ioannis T. Kassios |
| 2005 | Formal Aids for the Growth of Software Systems. | Mathai Joseph |
| 2005 | The Natural History of Bugs: Using Formal Methods to Analyse Software Related Failures in Space Missions. | Christopher W. Johnson |
| 2005 | On Partitioning and Symbolic Model Checking. | Subramanian K. Iyer, Debashis Sahoo, E. Allen Emerson, Jawahar Jain |
| 2005 | Model-Checking of Specifications Integrating Processes, Data and Time. | Jochen Hoenicke, Patrick Maier |
| 2005 | Floating-Point Verification. | John Harrison |
| 2005 | Formal Methods and Testing: Hypotheses, and Correctness Approximations. | Marie-Claude Gaudel |
| 2005 | Preliminary Results of a Case Study: Model Checking for Advanced Automotive Applications. | Stefan Eisler, Christian Scheidler, Bernhard Josko, Guido Sandmann, Joachim Stroop |
| 2005 | Automatic Symmetry Detection for Model Checking Using Computational Group Theory. | Alastair F. Donaldson, Alice Miller |
| 2005 | Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs. | Orieta Celiku, Annabelle McIver |
| 2005 | Control Law Diagrams in | Ana Cavalcanti, Phil Clayton, Colin O'Halloran |
| 2005 | Testing Concurrent Object-Oriented Systems with Spec Explorer. | Colin Campbell, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes |
| 2005 | Certified Memory Usage Analysis. | David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider |
| 2005 | Combining CSP and B for Specification and Property Verification. | Michael J. Butler, Michael Leuschel |
| 2005 | End-to-End Integrated Security and Performance Analysis on the DEGAS Choreographer Platform. | Mikael Buchholtz, Stephen Gilmore, Valentin Haenel, Carlo Montangero |
| 2005 | ASD Case Notes: Costs and Benefits of Applying Formal Methods to Industrial Control Software. | Guy H. Broadfoot |
| 2005 | Symbolic Animation of JML Specifications. | Fabrice Bouquet, Frdric Dadeau, Bruno Legeard, Mark Utting |
| 2005 | On Some Galois Connection Based Abstractions for the Mu-Calculus. | Dragan Bosnacki |
| 2005 | Adding Conflict and Confusion to CSP. | Christie Bolton |
| 2005 | Timed Testing with TorX. | Henrik C. Bohnenkamp, Axel Belinfante |
| 2005 | Verification of a Signature Architecture with HOL-Z. | David A. Basin, Hironobu Kuruma, Kazuo Takaragi, Burkhart Wolff |