iFM 2013

iFM 2013 Schedule

The detailed schedule of iFM 2013 is here.

Time scale Wednesday Time scale Thursday Time scale Friday

8:00-9:00 Registration open 8:00-9:00 Registration open 8:00-9:00 Registration open
8:45-9:00 Welcome from the Rector of Åbo Akademi University
9:00-10:00 Invited lecture: JR Abrial 9:00-10:00 Invited lecture: K Larsen 9:00-10:00 Invited lecture: C Laneve
10:00-10:30 Coffee break 10:00-10:30 Coffee break 10:00-10:30 Coffee break
10:30-12:30 Refinement, Integration, Translation 10:30-12:30 Reachability and Model Checking 10:30-12:30 Semantics
12:30-13:30 Lunch 12:30-13:30 Lunch 12:30-13:30 Lunch
13:30-14:30 Invited lecture: S Graf 13:30-15:00 Usability and testing 13:30-15:30 System-Level Analysis
14:30-15:00 Coffee break 15:00-15:10 Coffee break 15:30 Closing
15:00-17:00 Verification 15:10-16:10 Distributed systems 15:30-16:00 Coffee and goodbyes
17:00-17:30 Remembering Kaisa: E Sekerinski 16:25 Bus to herrankukkaro
19:00-20:30 Welcome reception 16:25-24:00 Social event

Invited speakers

From Z to B and then Event-B: Assigning Proofs to Meaningful Programs    Jean-Raymond Abrial

Knowledge for the Distributed Implementation of Constrained Systems    Susanne Graf

Priced Timed Automata and Statistical Model Checking    Kim Guldstrand Larsen

An Algebraic Theory for Web Service Contracts    Cosimo Laneve

Papers by sessions

Refinement, Integration, Translation

Progress Concerns as Design Guidelines    Thai Son Hoang and Simon Hudon
Assume-Guarantee Specifications of State Transition Diagrams for Behavioral Refinement    Christian Prehofer
Translating VDM to Alloy    Kenneth Lausdahl
Verification of EB3 Specifications using CADP    Dimitrios Vekris, Frederic Lang, Catalin Dima and Radu Mateescu


Automated Anonymity Verification of the ThreeBallot Voting System    Murat Moran, James Heather and Steve Schneider
Compositional Verification of Software Product Lines    Jean-Vivien Millo, Krishna Shankara Narayanan, Ganesh Narwane and S Ramesh
Deductive Verification of State-space Algorithms    Frédéric Gava, Jean Fortin and Michael Guedj
Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus    Daisuke Ishii, Guillaume Melquiond and Shin Nakajima

Reachability and Model Checking

Improved Reachability Analysis in DTMC via Divide and Conquer    Songzheng Song, Lin Gui, Jun Sun, Yang Liu and Jin Song Dong
Solving Games Using Incremental Induction    Andreas Morgenstern, Manuel Gesell and Klaus Schneider
Model-Checking Software Library API Usage Rules    Fu Song and Tayssir Touili
Formal Modelling and Verification of Population Protocols    Dominique Mery and Michael Poppleton

Usability and Testing

Detecting Vulnerabilities in Java-Card Bytecode Verifiers using Model-Based Testing    Aymerick Savary, Marc Frappier and Jean-Louis Lanet
Integrating Formal Predictions of Interactive System Behaviour with User Evaluation    Rimvydas Rukšėnas, Paul Curzon and Michael D. Harrison
Automatic Inference of Erlang Module Behaviour    Ramsay Taylor, Kirill Bogdanov and John Derrick

Distributed Systems

Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms    Manamiary Bruno Andriamiarina, Dominique Mery and Neeraj-Kumar Singh
Quantified Abstractions of Distributed Systems    Elvira Albert, Jesús Correas, German Puebla and Guillermo Román-Díez


A Compositional Automata-based Semantics for Property Patterns    Kalou Cabrera Castillos, Frederic Dadeau, Jacques Julliand, Bilal Kanso and Safouan Taha
A Formal Semantics for Complete UML State Machines with Communications    Shuang Liu, Yang Liu, Étienne André, Christine Choppy, Jun Sun, Bimlesh Wadhwa and Jin Song Dong
From Small-step Semantics to Big-step Semantics, Automatically    Stefan Ciobaca
Program Equivalence by Circular Reasoning    Dorel Lucanu and Vlad Rusu

System-Level Analysis

Structural Transformations for Data-Enriched Real-Time Systems    Ernst-Ruediger Olderog and Mani Swaminathan
Deadlock Analysis of Concurrent Objects: Theory and Practice    Elena Giachino, Carlo A. Grazia, Cosimo Laneve, Michael Lienhardt and Peter Y. H. Wong
Broadcast, Denial-of-Service, and Secure Communication    Roberto Vigo, Flemming Nielson and Hanne Riis Nielson
Characterizing Fault-Tolerant Systems by Means of Simulation Relations    Ramiro Demasi, Pablo Castro, Tom Maibaum and Nazareno Aguirre

Click on ICT-building Floor 1 map to enlarge.

Click on ICT-building Floor 3 map to enlarge.


  • 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.