| 2013 | Compositional Verification of Software Product Lines. | Jean-Vivien Millo, S. Ramesh, Shankara Narayanan Krishna, Ganesh Khandu Narwane |
| 2013 | Formal Modelling and Verification of Population Protocols. | Dominique Mry, Michael Poppleton |
| 2013 | Program Equivalence by Circular Reasoning. | Dorel Lucanu, Vlad Rusu |
| 2013 | A Formal Semantics for Complete UML State Machines with Communications. | Shuang Liu, Yang Liu, tienne Andr, Christine Choppy, Jun Sun, Bimlesh Wadhwa, Jin Song Dong |
| 2013 | Translating VDM to Alloy. | Kenneth Lausdahl |
| 2013 | Priced Timed Automata and Statistical Model Checking. | Kim Guldstrand Larsen |
| 2013 | An Algebraic Theory for Web Service Contracts. | Cosimo Laneve, Luca Padovani |
| 2013 | Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus. | Daisuke Ishii, Guillaume Melquiond, Shin Nakajima |
| 2013 | Systems Design Guided by Progress Concerns. | Simon Hudon, Thai Son Hoang |
| 2013 | Knowledge for the Distributed Implementation of Constrained Systems. | Susanne Graf, Sophie Quinton |
| 2013 | Deadlock Analysis of Concurrent Objects: Theory and Practice. | Elena Giachino, Carlo Augusto Grazia, Cosimo Laneve, Michael Lienhardt, Peter Y. H. Wong |
| 2013 | Deductive Verification of State-Space Algorithms. | Frdric Gava, Jean Fortin, Michal Guedj |
| 2013 | Characterizing Fault-Tolerant Systems by Means of Simulation Relations. | Ramiro Demasi, Pablo F. Castro, T. S. E. Maibaum, Nazareno Aguirre |
| 2013 | From Small-Step Semantics to Big-Step Semantics, Automatically. | Stefan Ciobaca |
| 2013 | A Compositional Automata-Based Semantics for Property Patterns. | Kalou Cabrera Castillos, Frdric Dadeau, Jacques Julliand, Bilal Kanso, Safouan Taha |
| 2013 | Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms. | Manamiary Bruno Andriamiarina, Dominique Mry, Neeraj Kumar Singh |
| 2013 | Quantified Abstractions of Distributed Systems. | Elvira Albert, Jess Correas, Germn Puebla, Guillermo Romn-Dez |
| 2013 | From Z to B and then Event-B: Assigning Proofs to Meaningful Programs. | Jean-Raymond Abrial |
| 2012 | Model Checking as Static Analysis: Revisited. | Fuyuan Zhang, Flemming Nielson, Hanne Riis Nielson |
| 2012 | Mechanized Extraction of Topology Anti-patterns in Wireless Networks. | Matthias Woehrle, Rena Bakhshi, Mohammad Reza Mousavi |
| 2012 | Behaviour-Based Cheat Detection in Multiplayer Games with Event-B. | HaiYun Tian, Phillip J. Brooke, Anne-Gwenn Bosser |
| 2012 | Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B. | Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis |
| 2012 | Patterns for a Log-Based Strengthening of Declarative Compliance Models. | Dennis M. M. Schunselaar, Fabrizio Maria Maggi, Natalia Sidorova |
| 2012 | A Formal Interactive Verification Environment for the Plan Execution Interchange Language. | Camilo Rocha, Hctor Cadavid, Csar A. Muoz, Radu Siminiceanu |
| 2012 | Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples. | Herbert Rocha, Raimundo S. Barreto, Lucas C. Cordeiro, Arilo Dias Neto |