iFM 2013


10th International Conference on integrated Formal Methods (iFM 2013)
June 10 - 14, 2013 - Turku, Finland

WELCOME to iFM 2013!!

- Conference: 12-14.6.2013
- Co-located workshops and tutorials: 10-11.6.2013

The registration to iFM 2013 can be done on the web:

The iFM schedule is here:

- Jean-Raymond Abrial, Marseille, France:
From Z to B and then Event-B: Assigning Proofs to Meaningful Programs
- Susanne Graf, VERIMAG, France:
Knowledge for the Distributed Implementation of Constrained Systems
- Kim Larsen, Aalborg University, Denmark:
Priced Timed Automata and Statistical Model Checking
- Cosimo Laneve, University of Bologna, Italy:
An Algebraic Theory for Web Service Contracts

This edition of the integrated Formal Methods conference is dedicated to Professor Kaisa Sere, Åbo Akademi University (1954-2012).
Professor Emil Sekerinski, one of Kaisa's closest scientific collaborators, will give a short lecture for remembering Kaisa.

Applying formal methods may involve modeling different aspects of a system which are best expressed using different formalisms. Correspondingly, different analysis techniques may be used to examine different system views, different kinds of properties, or, simply in order to cope with the sheer complexity of the system. The iFM conference series seeks to further research into hybrid approaches to formal modeling and analysis; i.e., the combination of (formal and semi-formal) methods for system development, regarding modeling and analysis, and covering all aspects from language design through verification and analysis techniques to tools and their integration into software engineering practice.

25 regular papers will be presented at the conference:
1. Thai Son Hoang and Simon Hudon. Progress Concerns as Design Guidelines
2. Christian Prehofer. Assume-Guarantee Specifications of State Transition Diagrams for Behavioral Refinement
3. Kenneth Lausdahl. Translating VDM to Alloy
4. Dimitrios Vekris, Frederic Lang, Catalin Dima and Radu Mateescu. Verification of EB3 Specification using CADP
5. Murat Moran, James Heather and Steve Schneider. Automated Anonymity Verification of ThreeBallot Voting System
6. Jean-Vivien Millo, Krishna S, Ganesh Narwane and S Ramesh. Compositional Verification of Software Product Lines
7. Frédéric Gava, Jean Fortin and Michael Guedj. Deductive Verification of State-space Algorithms
8. Daisuke Ishii, Guillaume Melquiond and Shin Nakajima. Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus
9. Songzheng Song, Lin Gui, Jun Sun, Yang Liu and Jin Song Dong. Improved Reachability Analysis in DTMC via Divide and Conquer
10. Andreas Morgenstern, Manuel Gesell and Klaus Schneider. Solving Games Using Incremental Induction
11. Fu Song and Tayssir Touili. Model-Checking Software Library API Usage Rules
12. Dominique Mery and Michael Poppleton. Formal Modelling and Verification of Population Protocols
13. Aymerick Savary, Marc Frappier and Jean-Louis Lanet. Detecting Vulnerabilities in Java-Card Bytecode verifiers using Model-Based Testing
14. Rimvydas Rukšenas, Paul Curzon and Michael D. Harrison. Integrating Formal Predictions of Interactive System Behaviour with User Evaluation
15. Ramsay Taylor, Kirill Bogdanov and John Derrick. Automatic Inference of Erlang Module Behaviour
16. Manamiary Bruno Andriamiarina, Dominique Mery and Neeraj-Kumar Singh. Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms
17. Elvira Albert, Jesús Correas, German Puebla and Guillermo Román-Díez. Quantified Abstractions of Distributed Systems
18. Kalou Cabrera Castillos, Frederic Dadeau, Jacques Julliand, Bilal Kanso and Safouan Taha. A Compositional Automata-based Semantics for Property Patterns
19. Shuang Liu, Yang Liu, Étienne André, Christine Choppy, Jun Sun, Bimlesh Wadhwa and Jin Song Dong. A Formal Semantics for Complete UML State Machines with Communications 20. Stefan Ciobaca. From Small-step Semantics to Big-step Semantics, Automatically
21. Dorel Lucanu and Vlad Rusu. Program Equivalence by Circular Reasoning
22. Ernst-Ruediger Olderog and Mani Swaminathan. Structural Transformations for Data-Enriched Real-Time Systems
23. Elena Giachino, Carlo A. Grazia, Cosimo Laneve, Michael Lienhardt and Peter Y. H. Wong. Deadlock Analysis of Concurrent Objects: Theory and Practice
24. Roberto Vigo, Flemming Nielson and Hanne Riis Nielson. Broadcast, Denial-of-Service, and Secure Communication
25. Ramiro Demasi, Pablo Castro, Tom Maibaum and Nazareno Aguirre. Characterizing Fault-Tolerant Systems by Means of Simulation Relations

iFM 2013 is accompanied by the following workshops and tutorials:
- 4th International Workshop on Computational Models for Cell Processes, CompMod 2013:
- 4th Rodin User and Developer Workshop, Rodin 2013:
- 16th BCS FACS Refinement Workshop 2013, REFINE 2013:
- Tutorial: Specification and Proof of Programs with Frama-C:

- Einar Broch Johnsen, University of Oslo, Norway
- Luigia Petre, Åbo Akademi University, Finland

Pontus Boström, Åbo Akademi University, Finland

Luigia Petre, Åbo Akademi University, Finland

- Erika Abraham, RWTH Aachen University, Germany;
- Elvira Albert, Complutense University of Madrid, Spain;
- Marcello Bonsangue, Leiden University, the Netherlands;
- Phillip J Brooke, Teesside University, UK;
- Ana Cavalcanti, University of York, UK;
- Dave Clarke, Catholic University of Leuven, Belgium;
- John Derrick, Unversity of Sheffield, UK;
- Jin Song Dong, National University of Singapore, Singapore;
- Kerstin Eder, University of Bristol, UK;
- John Fitzgerald, Newcastle University, UK;
- Andy Galloway, University of York, UK;
- Marieke Huisman, University of Twente, the Netherlands;
- Reiner Hähnle, Technical University of Darmstadt, Germany;
- Einar Broch Johnsen, University of Oslo, Norway;
- Peter Gorm Larsen, Aarhus University, Denmark;
- Diego Latella, ISTI-CNR, Pisa, Italy;
- Michael Leuschel, University of Duesseldorf, Germany;
- Shaoying Liu, Hosei University, Japan;
- Michele Loreti, University of Florence, Italy;
- Dominique Mery, LORIA and University of Lorraine, France;
- Stephan Merz, INRIA Lorraine, France;
- Richard Paige, University of York, UK;
- Luigia Petre, Åbo Akademi University, Finland;
- Kristin Yvonne Rozier, NASA Ames Research Center, USA;
- Philipp Ruemmer, Uppsala University, Sweden;
- Thomas Santen, European Microsoft Innovation Center, Germany;
- Ina Schaefer, Technical University of Braunschweig, Germany;
- Steve Schneider, University of Surrey, UK;
- Emil Sekerinski, McMaster University, Canada;
- Graeme Smith, University of Queensland, Australia;
- Colin Snook, University of Southampton, UK;
- Kenji Taguchi, AIST, Japan;
- Helen Treharne, University of Surrey, UK;
- Heike Wehrheim, University of Paderborn, Germany;
- Herbert Wiklicky, Imperial College, UK;
- Gianluigi Zavattaro, University of Bologna, Italy

This call for participation and additional information about the conference can be found at
For information regarding the conference you can contact:


  • 1.7.2013
    Susanne Graf's pictures from iFM 2013 are now available.
  • 27.6.2013
    Videos are now available.
  • 18.6.2013
    Photos from all days are now available.
  • 10.6.2013
    The detailed schedule of iFM 2013 is here.
  • 10.6.2013
    Maps of Turku city and ICT-building has been added.
  • 10.6.2013
    Social event program updated.
  • 6.6.2013
    The Rector of Åbo Akademi University, Professor Jorma Mattinen will kindly open iFM 2013, on June 12, at 8:45 in Auditorium Alpha!
  • 4.6.2013
    The Åbo Akademi University magazine "Meddelanden" reported (in Swedish) about iFM 2013 here.
  • 23.05.2013
    The proceedings of iFM 2013 (LNCS 7940) is now accessible from Springer, here.
  • 22.4.2013
    The schedule and the list of accepted papers (with abstracts) have been uploaded.
  • 26.3.2013
    Registration has opened!
  • 11.1.2013
    We have extended the paper submission deadline to 27.1.2013!
  • 19.11.2012
    We are very happy to announce that the following TWO renowned Springer journals have kindly accepted to host special issues of iFM 2013: Formal Aspects of Computing and Software and Systems Modeling.
  • 12.11.2012
    We have the pleasure of confirming the following invited speakers at iFM 2013: Jean-Raymond Abrial, Cosimo Laneve, Susanne Graf, and Kim Larsen.
  • 31.10.2012
    We have now booked the lovely venue of Herrankukkaro for the social event on 13.6.2013. We will go to a fishing village close to Turku, where we will walk around, take a (smoke) sauna, and enjoy a nice dinner. We will go there by bus and come back by boat, enjoying the light nights of June in Finland. You can check more about it here.