| 2009 | Overflow and Roundoff Error Analysis via Model Checking. | Do Thi Bich Ngoc, Mizuhito Ogawa |
| 2009 | Refinement via Interpretation. | Manuel A. Martins, Alexandre Madeira, Lus Soares Barbosa |
| 2009 | Formal Modeling and Analysis of an IETF Multicast Protocol. | Elisabeth Lien, Peter Csaba lveczky |
| 2009 | Programming Sagas in SOCK. | Ivan Lanese, Gianluigi Zavattaro |
| 2009 | Specifying and Checking Refinement Relationships in VDM++. | Yojiro Kawamata, Christian Sommer, Fuyuki Ishikawa, Shinichi Honiden |
| 2009 | Relational Interprocedural Verification of Concurrent Programs. | Bertrand Jeannet |
| 2009 | Behavioral Specification of Reactive Systems Using Stream-Based I/O Tables. | Benjamin Hummel, Judith Thyssen |
| 2009 | Event-B Patterns and Their Tool Support. | Thai Son Hoang, Andreas Frst, Jean-Raymond Abrial |
| 2009 | Simulation Relations for Systems with Distributed Interfaces. | Robert M. Hierons, Manuel Nez |
| 2009 | Checking Sequence Construction Using Adaptive and Preset Distinguishing Sequences. | Robert M. Hierons, Guy-Vincent Jourdan, Hasan Ural, Hsn Yenign |
| 2009 | Modal Contracts for Component-Based Design. | Gregor Goessler, Jean-Baptiste Raclet |
| 2009 | Checkmate: A Generic Static Analyzer of Java Multithreaded Programs. | Pietro Ferrara |
| 2009 | An Automated Approach to Verifying Diagnosability in Multi-agent Systems. | Jonathan Ezekiel, Alessio Lomuscio |
| 2009 | Ontology-Based Reasoning in Requirements Elicitation. | Dang Viet Dzung, Atsushi Ohnishi |
| 2009 | Implementation Correctness of a Real-Time Operating System. | Matthias Daum, Norbert Schirmer, Mareike Schmidt |
| 2009 | Precise Model-Driven Transformations Based on Graphs and Metamodels. | Duc-Hanh Dang, Martin Gogolla |
| 2009 | Mapping between Alloy Specifications and Database Implementations. | Alcino Cunha, Hugo Pacheco |
| 2009 | LARVA --- Safer Monitoring of Real-Time Java Programs (Tool Paper). | Christian Colombo, Gordon J. Pace, Gerardo Schneider |
| 2009 | Specifying Interacting Components with Coordinated Concurrent Scenarios. | Prakash Chandrasekaran, Madhavan Mukund |
| 2009 | Adjusted Verification Rules for Loops Are More Complete and Give Better Diagnostics for Less. | Patrice Chalin |
| 2009 | Heuristic Sensitivity in Guided Random-Walk Based Model Checking. | Thang H. Bui, Albert Nymeyer |
| 2009 | Right Propositional Neighborhood Logic over Natural Numbers with Integer Constraints for Interval Lengths. | Davide Bresolin, Valentin Goranko, Angelo Montanari, Guido Sciavicco |
| 2009 | Property-Driven Scenario Integration. | Jewgenij Botaschanjan, Alexander Harhurin |
| 2009 | A Computability Perspective on Self-Modifying Programs. | Guillaume Bonfante, Jean-Yves Marion, Daniel Reynaud-Plantey |
| 2009 | Using Probabilistic Model Checking to Evaluate GUI Testing Techniques. | Cristiano Bertolini, Alexandre Mota |