iFM 2013

Workshops and Tutorials

Workshop dates: 10-11 June 2013.

The 4th International Workshop on Computational Models for Cell Processes (CompMod 2013)

Ion Petre, ipetre 'at'

Computational systems biology is an exciting new application area for applied mathematics and computer science. This workshop of the 10th International Conference on integrated Formal Methods (iFM) fosters an excellent platform gathering researchers in formal methods and related fields that are interested in the wealth of opportunities and challenges in systems biology.

Rodin User and Developer Workshop 2013

Michael Butler, University of Southampton
Stefan Hallerstede, Aarhus University
Thierry Lecomte, ClearSy
Michael Leuschel, University of Düsseldorf
Alexander Romanovsky, University of Newcastle
Laurent Voisin, Systerel
Marina Walden, Åbo Akademi

Event-B is a formal method for system-level modelling and analysis. The Rodin Platform is an Eclipse-based toolset for Event-B that provides effective support for modelling and automated proof. The platform is open source and is further extendable with plug-ins. A range of plug-ins have already been developed including ones that support animation, model checking and UML-B. While much of the development and use of Rodin takes place within EU FP7 Projects (RODIN, DEPLOY, ADVANCE), there is a growing group of users and plug-in developers outside these projects. The purpose of this workshop is to bring together existing and potential users and developers of the Rodin toolset and to foster a broader community of Rodin users and developers.

BCS FACS 2013 Refinement Workshop 2013

Eerke Boiten, University of Kent, UK
John Derrick, University of Sheffield, UK
Steve Reeves, University of Waikato, NZ

Refinement is one of the cornerstones of a formal approach to software engineering: the process of developing a more detailed design or implementation from an abstract specification through a sequence of mathematically-based steps that maintain correctness with respect to the original specification. The aim of this BCS FACS Refinement Workshop, is to bring together people who are interested in the development of more concrete designs or executable programs from abstract specifications using formal notations, tool support for formal software development, and practical experience with formal refinement methodologies.

Tutorial: Specification and Proof of Programs with Frama-C

Nikolai Kosmatov, Software Safety Laboratory, CEA LIST, France
Virgile Prevosto, Software Safety Laboratory, CEA LIST, France
Julien Signoles, Software Safety Laboratory, CEA LIST, France

Despite the spectacular progress made by the developers of formal verification tools, their usage remains basically reserved for the most critical software. More and more engineers and researchers today are interested in such tools in order to integrate them into their everyday work. This half-day tutorial proposes a practical introduction during which the participants will write C program specifications, observe the proof results, analyze proof failures and fix them. Participants will be taught how to write a specification for a C program, in the form of function contracts, and easily prove it with an automatic tool in FRAMA-C, a freely available software verification toolset. Those who will have FRAMA-C and JESSIE installed (e.g. from ready-to-install packages frama-c, why, alt-ergo under Linux) will also run automatic proof of programs on their computer. Program specifications will be written in the specification language ACSL similar to other specification languages like JML that some participants may know. ACSL-syntax is intentionally close to C and can be easily learned on-the-fly.

The tutorial is aimed mainly at software engineering students and professionals who will learn more about the state of the art in automated software verification and how it could help them in their career in software development or validation. Using freely available tools FRAMA-C and JESSIE will allow them to quickly install and try the tools. Software engineering lecturers will also be interested in how a tool such as FRAMA-C can help in teaching software verification. The only necessary background is some familiarity with the C language.

FRAMA-C tutorial will be held on Tuesday afternoon and the registration can be done at the iFM 2013 registration or the dedicated FRAMA-C registration for those who do not wish to register to iFM 2013 at the same time.

12:30 - 13:30: Lunch
13.30 - 14:15: Presentation of the Frama-C platform
14:15 - 15:15: Basic specification and verification with WP plug-in
15:15 - 15:45: Coffee break
15:45 - 16:30: Loop invariant and variant
16:30 - 17:30: Advanced specification and verification

Material from the tutorial can be found at:

The Overture and FMDEP workshops have been cancelled!


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