| 2013 | A Compositional Automata-Based Semantics for Property Patterns. Kalou Cabrera Castillos, Frédéric Dadeau, Jacques Julliand, Bilal Kanso, Safouan Taha |
| 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 | An Algebraic Theory for Web Service Contracts. Cosimo Laneve, Luca Padovani |
| 2013 | Assume-Guarantee Specifications of State Transition Diagrams for Behavioral Refinement. Christian Prehofer |
| 2013 | Automated Anonymity Verification of the ThreeBallot Voting System. Murat Moran, James Heather, Steve A. Schneider |
| 2013 | Automatic Inference of Erlang Module Behaviour. Ramsay Taylor, Kirill Bogdanov, John Derrick |
| 2013 | Broadcast, Denial-of-Service, and Secure Communication. Roberto Vigo, Flemming Nielson, Hanne Riis Nielson |
| 2013 | Characterizing Fault-Tolerant Systems by Means of Simulation Relations. Ramiro Demasi, Pablo F. Castro, T. S. E. Maibaum, Nazareno Aguirre |
| 2013 | Compositional Verification of Software Product Lines. Jean-Vivien Millo, S. Ramesh, Shankara Narayanan Krishna, Ganesh Khandu Narwane |
| 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. Frédéric Gava, Jean Fortin, Michaël Guedj |
| 2013 | Detecting Vulnerabilities in Java-Card Bytecode Verifiers Using Model-Based Testing. Aymerick Savary, Marc Frappier, Jean-Louis Lanet |
| 2013 | Formal Modelling and Verification of Population Protocols. Dominique Méry, Michael Poppleton |
| 2013 | From Small-Step Semantics to Big-Step Semantics, Automatically. Stefan Ciobaca |
| 2013 | From Z to B and then Event-B: Assigning Proofs to Meaningful Programs. Jean-Raymond Abrial |
| 2013 | Improved Reachability Analysis in DTMC via Divide and Conquer. Songzheng Song, Lin Gui, Jun Sun, Yang Liu, Jin Song Dong |
| 2013 | Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus. Daisuke Ishii, Guillaume Melquiond, Shin Nakajima |
| 2013 | Integrated Formal Methods, 10th International Conference, IFM 2013, Turku, Finland, June 10-14, 2013. Proceedings Einar Broch Johnsen, Luigia Petre |
| 2013 | Integrating Formal Predictions of Interactive System Behaviour with User Evaluation. Rimvydas Ruksenas, Paul Curzon, Michael D. Harrison |
| 2013 | Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms. Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh |
| 2013 | Knowledge for the Distributed Implementation of Constrained Systems. Susanne Graf, Sophie Quinton |
| 2013 | Model-Checking Software Library API Usage Rules. Fu Song, Tayssir Touili |
| 2013 | Priced Timed Automata and Statistical Model Checking. Kim Guldstrand Larsen |
| 2013 | Program Equivalence by Circular Reasoning. Dorel Lucanu, Vlad Rusu |
| 2013 | Quantified Abstractions of Distributed Systems. Elvira Albert, Jesús Correas, Germán Puebla, Guillermo Román-Díez |
| 2013 | Solving Games Using Incremental Induction. Andreas Morgenstern, Manuel Gesell, Klaus Schneider |
| 2013 | Structural Transformations for Data-Enriched Real-Time Systems. Ernst-Rüdiger Olderog, Mani Swaminathan |
| 2013 | Systems Design Guided by Progress Concerns. Simon Hudon, Thai Son Hoang |
| 2013 | Translating VDM to Alloy. Kenneth Lausdahl |
| 2013 | Verification of EB Dimitris Vekris, Frédéric Lang, Catalin Dima, Radu Mateescu |