| 2009 | An Introduction to Grammar Convergence. Ralf Lämmel, Vadim Zaytsev |
| 2009 | Application of Graph Transformation in Verification of Dynamic Systems. Zarrin Langari, Richard J. Trefler |
| 2009 | Automatic Generation of Error Messages for the Symbolic Execution of EB3 Process Expressions. Jérémy Milhau, Benoît Fraikin, Marc Frappier |
| 2009 | CSP with Hierarchical State. Robert Colvin, Ian J. Hayes |
| 2009 | Challenges in the Specification of Full Contracts. Gordon J. Pace, Gerardo Schneider |
| 2009 | Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B. Steve A. Schneider, Helen Treharne |
| 2009 | Decomposition Structures for Event-B. Michael J. Butler |
| 2009 | Decompositional Petri Net Reductions. Astrid Rakow |
| 2009 | Developing Topology Discovery in Event-B. Thai Son Hoang, Hironobu Kuruma, David A. Basin, Jean-Raymond Abrial |
| 2009 | Dynamic Path Reduction for Software Model Checking. Zijiang Yang, Bashar Al-Rawi, Karem A. Sakallah, Xiaowan Huang, Scott A. Smolka, Radu Grosu |
| 2009 | Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays. Osman Hasan, Naeem Abbasi, Sofiène Tahar |
| 2009 | Formal Verification Based on Guided Random Walks. Thang H. Bui, Albert Nymeyer |
| 2009 | Incremental Reasoning for Multiple Inheritance. Johan Dovland, Einar Broch Johnsen, Olaf Owe, Martin Steffen |
| 2009 | Integrated Formal Methods, 7th International Conference, IFM 2009, Düsseldorf, Germany, February 16-19, 2009. Proceedings Michael Leuschel, Heike Wehrheim |
| 2009 | Mechanised Translation of Control Law Diagrams into Circus. Frank Zeyda, Ana Cavalcanti |
| 2009 | Model Checking LTL Formulae in RAISE with FDR. Abigail Parisaca Vargas, Ana Gabriela Garis, Silvia Lizeth Tapia Tarifa, Chris George |
| 2009 | Modelling Divergence in Relational Concurrent Refinement. Eerke A. Boiten, John Derrick |
| 2009 | Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format. Jan Stöcker, Frédéric Lang, Hubert Garavel |
| 2009 | Partial Order Reduction for State/Event LTL. Nikola Benes, Lubos Brim, Ivana Cerná, Jiri Sochor, Pavlína Vareková, Barbora Zimmerová |
| 2009 | Predicate Abstraction in a Program Logic Calculus. Benjamin Weiß |
| 2009 | Property Specifications for Workflow Modelling. Peter Y. H. Wong, Jeremy Gibbons |
| 2009 | Realizability of Choreographies Using Process Algebra Encodings. Gwen Salaün, Tevfik Bultan |
| 2009 | SAL-Based Symbolic Scheduling in Time-Triggered Networks. Sebastian Voss, Maria Sorea, Klaus Echtle |
| 2009 | Taming the Unbounded for Hardware Synthesis. Byron Cook |
| 2009 | Verifying UML/OCL Operation Contracts. Jordi Cabot, Robert Clarisó, Daniel Riera |