| 2009 | A Computability Perspective on Self-Modifying Programs. Guillaume Bonfante, Jean-Yves Marion, Daniel Reynaud-Plantey |
| 2009 | Adjusted Verification Rules for Loops Are More Complete and Give Better Diagnostics for Less. Patrice Chalin |
| 2009 | An Automated Approach to Verifying Diagnosability in Multi-agent Systems. Jonathan Ezekiel, Alessio Lomuscio |
| 2009 | Applying Formal Passive Testing to Study Temporal Properties of the Stream Control Transmission Protocol. César Andrés, Mercedes G. Merayo, Manuel Núñez |
| 2009 | Behavioral Specification of Reactive Systems Using Stream-Based I/O Tables. Benjamin Hummel, Judith Thyssen |
| 2009 | Checking Sequence Construction Using Adaptive and Preset Distinguishing Sequences. Robert M. Hierons, Guy-Vincent Jourdan, Hasan Ural, Hüsnü Yenigün |
| 2009 | Checkmate: A Generic Static Analyzer of Java Multithreaded Programs. Pietro Ferrara |
| 2009 | Completeness of Pointer Program Verification by Separation Logic. Makoto Tatsuta, Wei-Ngan Chin, Mahmudul Faisal Al Ameen |
| 2009 | Coordinated Consensus Analysis of Multi-agent Systems Using Event-B. Ninh-Thuan Truong, Thanh-Binh Trinh, Viet Ha Nguyen |
| 2009 | Event-B Patterns and Their Tool Support. Thai Son Hoang, Andreas Fürst, Jean-Raymond Abrial |
| 2009 | Formal Modeling and Analysis of an IETF Multicast Protocol. Elisabeth Lien, Peter Csaba Ölveczky |
| 2009 | Heuristic Sensitivity in Guided Random-Walk Based Model Checking. Thang H. Bui, Albert Nymeyer |
| 2009 | Implementation Correctness of a Real-Time Operating System. Matthias Daum, Norbert Schirmer, Mareike Schmidt |
| 2009 | Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms. Marcello M. Bersani, Carlo A. Furia, Matteo Pradella, Matteo Rossi |
| 2009 | LARVA --- Safer Monitoring of Real-Time Java Programs (Tool Paper). Christian Colombo, Gordon J. Pace, Gerardo Schneider |
| 2009 | Mapping between Alloy Specifications and Database Implementations. Alcino Cunha, Hugo Pacheco |
| 2009 | Modal Contracts for Component-Based Design. Gregor Goessler, Jean-Baptiste Raclet |
| 2009 | Ontology-Based Reasoning in Requirements Elicitation. Dang Viet Dzung, Atsushi Ohnishi |
| 2009 | Overflow and Roundoff Error Analysis via Model Checking. Do Thi Bich Ngoc, Mizuhito Ogawa |
| 2009 | Precise Model-Driven Transformations Based on Graphs and Metamodels. Duc-Hanh Dang, Martin Gogolla |
| 2009 | Programming Sagas in SOCK. Ivan Lanese, Gianluigi Zavattaro |
| 2009 | Property-Driven Scenario Integration. Jewgenij Botaschanjan, Alexander Harhurin |
| 2009 | Refinement via Interpretation. Manuel A. Martins, Alexandre Madeira, Luís Soares Barbosa |
| 2009 | Relational Interprocedural Verification of Concurrent Programs. Bertrand Jeannet |
| 2009 | Right Propositional Neighborhood Logic over Natural Numbers with Integer Constraints for Interval Lengths. Davide Bresolin, Valentin Goranko, Angelo Montanari, Guido Sciavicco |
| 2009 | Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009, Hanoi, Vietnam, 23-27 November 2009 Dang Van Hung, Padmanabhan Krishnan |
| 2009 | Simulation Relations for Systems with Distributed Interfaces. Robert M. Hierons, Manuel Núñez |
| 2009 | Software Verification and System Assurance. John M. Rushby |
| 2009 | Specifying Interacting Components with Coordinated Concurrent Scenarios. Prakash Chandrasekaran, Madhavan Mukund |
| 2009 | Specifying and Checking Refinement Relationships in VDM++. Yojiro Kawamata, Christian Sommer, Fuyuki Ishikawa, Shinichi Honiden |
| 2009 | Using Change Impact Analysis to Select Tests for Extended Finite State Machines. Mahadevan Subramaniam, Bo Guo, Zoltán Pap |
| 2009 | Using Probabilistic Model Checking to Evaluate GUI Testing Techniques. Cristiano Bertolini, Alexandre Mota |