| 2009 | A Compositional Approach on Modal Specifications for Timed Systems. Nathalie Bertrand, Axel Legay, Sophie Pinchinat, Jean-Baptiste Raclet |
| 2009 | A Graph-Based Operational Semantics of OO Programs. Wei Ke, Zhiming Liu, Shuling Wang, Liang Zhao |
| 2009 | A Lazy Unbounded Model Checker for Event-B. Paulo J. Matos, Bernd Fischer, João Marques-Silva |
| 2009 | A Statistical Approach to Test Stochastic and Probabilistic Systems. Mercedes G. Merayo, Iksoon Hwang, Manuel Núñez, Ana R. Cavalli |
| 2009 | A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. Jiri Barnat, Lubos Brim, Petr Rockai |
| 2009 | A Verification System for Distributed Objects with Asynchronous Method Calls. Wolfgang Ahrendt, Maximilian Dylla |
| 2009 | Algorithmic Verification with Multiple and Nested Parameters. Antti Siirtola, Juha Kortelainen |
| 2009 | An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata. Joakim Byg, Kenneth Yrke Jørgensen, Jirí Srba |
| 2009 | An Empirical Study of Structural Constraint Solving Techniques. Junaid Haroon Siddiqui, Sarfraz Khurshid |
| 2009 | Approximate Model Checking of PCTL Involving Unbounded Path Properties. Samik Basu, Arka P. Ghosh, Ru He |
| 2009 | Bounded Semantics of CTL and SAT-Based Verification. Wenhui Zhang |
| 2009 | Circular Coinduction with Special Contexts. Dorel Lucanu, Grigore Rosu |
| 2009 | Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language. Anil Madhavapeddy |
| 2009 | Compositional Verification of Input-Output Conformance via CSP Refinement Checking. Augusto Sampaio, Sidney C. Nogueira, Alexandre Mota |
| 2009 | Development of Security Software: A High Assurance Methodology. David S. Hardin, T. Douglas Hiratzka, D. Randolph Johnson, Lucas G. Wagner, Michael W. Whalen |
| 2009 | European Train Control System: A Case Study in Formal Verification. André Platzer, Jan-David Quesel |
| 2009 | Event Listener Analysis and Symbolic Execution for Testing GUI Applications. Svetoslav R. Ganov, Chip Killmar, Sarfraz Khurshid, Dewayne E. Perry |
| 2009 | Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings Karin K. Breitman, Ana Cavalcanti |
| 2009 | Graded-CTL: Satisfiability and Symbolic Model Checking. Alessandro Ferrante, Margherita Napoli, Mimmo Parente |
| 2009 | Implementing a Direct Method for Certificate Translation. Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet |
| 2009 | Implementing and Applying the Stocks-Carrington Framework for Model-Based Testing. Maximiliano Cristiá, Pablo Rodríguez Monetti |
| 2009 | Improving Automatic Verification of Security Protocols with XOR. Xihui Chen, Ton van Deursen, Jun Pang |
| 2009 | Machine-Checked Sequencer for Critical Embedded Code Generator. Nassima Izerrouken, Marc Pantel, Xavier Thirioux |
| 2009 | Modal Systems: Specification, Refinement and Realisation. Fernando Luís Dotti, Alexei Iliasov, Leila Ribeiro, Alexander B. Romanovsky |
| 2009 | Modeling and Analysis of Thread-Pools in an Industrial Communication Platform. Frank S. de Boer, Immo Grabe, Mohammad Mahdi Jaghoori, Andries Stam, Wang Yi |
| 2009 | Modeling and Verification of Privacy Enhancing Protocols. Suriadi Suriadi, Chun Ouyang, Jason Smith, Ernest Foo |
| 2009 | Proof Assisted Model Checking for B. Jens Bendisposto, Michael Leuschel |
| 2009 | Qualitative Action Systems. Bernhard K. Aichernig, Harald Brandl, Willibald Krenn |
| 2009 | RAFFS: Model Checking a Robust Abstract Flash File Store. Paul Taverne, Cornelis Pronk |
| 2009 | Refinement-Preserving Co-evolution. Thomas Ruhroth, Heike Wehrheim |
| 2009 | Role-Based Symmetry Reduction of Fault-Tolerant Distributed Protocols with Language Support. Péter Bokor, Marco Serafini, Neeraj Suri, Helmut Veith |
| 2009 | Scalable Multi-core Model Checking Fairness Enhanced Systems. Yang Liu, Jun Sun, Jin Song Dong |
| 2009 | Seamless Model Driven Systems Engineering Based on Formal Models. Manfred Broy |
| 2009 | Specifying and Verifying Business Processes Using PPML. Germán Regis, Nazareno Aguirre, T. S. E. Maibaum |
| 2009 | Supporting Reuse of Event-B Developments through Generic Instantiation. Renato Silva, Michael J. Butler |
| 2009 | Symbolic Query Exploration. Margus Veanes, Pavel Grigorenko, Peli de Halleux, Nikolai Tillmann |
| 2009 | The VSE Refinement Method in Hets. Mihai Codescu, Bruno Langenstein, Christian Maeder, Till Mossakowski |
| 2009 | Verifying Ptolemy II Discrete-Event Models Using Real-Time Maude. Kyungmin Bae, Peter Csaba Ölveczky, Thomas Huining Feng, Stavros Tripakis |
| 2009 | Verifying Stateful Timed CSP Using Implicit Clocks and Zone Abstraction. Jun Sun, Yang Liu, Jin Song Dong, Xian Zhang |