HTTP/1.1 200 OK Date: Mon, 19 Jan 2026 03:53:28 GMT Server: Apache X-Frame-Options: SAMEORIGIN Strict-Transport-Security: max-age=31536000; includeSubDomains; preload Last-Modified: Tue, 14 Oct 2025 16:32:54 GMT ETag: "7b2c-64120ef942450" Accept-Ranges: bytes Content-Length: 31532 X-Frame-Options: sameorigin Connection: close Content-Type: text/html; charset=ISO-8859-1

ERCIM Working Group on Formal Methods for Industrial Critical Systems (FMICS)

Home Page

---

Recent and Forthcoming Events (updated 2025/10/14)

• FMICS 2026 - September 1-5, 2026 - Liverpool, UK
• Report on FMICS 2025
• FMICS 2025 - August 27-28, 2025 - Aarhus, Denmark
• Maurice ter Beek elected as the new FMICS chair (Oct. 2022)
• The 2020 Expert Survey on Formal Methods
• ERCIM News
• ERCIM "Alain Bensoussan" Fellowship Programme

---

Table of contents

• ERCIM's oldest active Working Group
• Background
• Objectives
• Scientific Activities
• Best Paper Awards
• Official ERCIM Documents about FMICS
• Contacts
• Institutions and Participants

---

1.      ERCIM's oldest active Working Group

Following an initial successful workshop bringing together ERCIM members interested in formal verification, held in Pisa in December 1992, Stefania Gnesi and Diego Latella, CNR, Pisa, proposed to create an ERCIM working group dedicated to Formal Methods for Industrial Critical Systems (FMICS). Although at that time, model checking was in its early days, the early ERCIM FMICS community was already aware of the great potential of formal verification techniques.

Since then, the WG, chaired in succession by Diego Latella (ISTI-CNR), Hubert Garavel (INRIA), Stefania Gnesi (ISTI), Pedro Merino (SparCIM), Alessandro Fantechi (ISTI), Radu Mateescu (INRIA), and Tiziana Margaria (LERO), has kept pace with the development of formal verification techniques - and model checking in particular. The series of annual workshops, began in 1996 and sponsored by the WG, have promoted an ongoing scientific discussion focussed on identifying the most efficient verification techniques, with a keen eye to their industrial applicability. Most of the members of the FMICS community have strong links with industry and have thus contributed to the slow but constant introduction of formal methods in the development cycle of industrial critical systems witnessed in the last decade. The WG has also addressed other readily applicable verification techniques, such as static analysis by abstract interpretation. Similarly, the whole formal development lifecycle has been addressed, for example in the 2008 FMICS workshop where considerable attention was paid to the recent diffusion of Model Driven Development in industry.

In 2008, issue number 75 of the ERCIM News hosted a joint special session edited by Pedro Merino, coordinator of the WG, and Erwin Schoitsch, coordinator of the DES Dependable Embedded System WG, featuring almost 30 articles, many of which reporting advances on the application of formal methods in industry.

The FMICS workshop series has always been open to contributions from outside the ERCIM community, and strong links have been maintained with other organizations, such as Formal Methods Europe. In November 2009, the FMICS workshop was held during the FM week, a special gathering of events organized this year by the FME association.

---

2.      Background

Formal methods have been advocated as a means of increasing the reliability of systems, especially those which are safety or business critical, but the industrial uptake of such methods has been slow. This is due to the perceived difficulty of mathematical nature of these methods, the lack of tool support, and the lack of precedents where formal methods has been proven to be effective. It is even more difficult to develop automatic specification and verification tools due to limitations like state explosion, undecidability, etc. This working group will bring together researchers of the ERCIM consortium in order to promote the use of formal methods within industry.

The behaviour of reactive systems is largely conditioned by the interaction with events of the external environment the sequentialization of which is not predictable. The complexity of the systems' behaviour increases considerably when the timing dependencies in the execution of events are taken into account.

The above features are typical of a large class of systems including control systems, automation systems, and communication systems and results in the extreme difficulty of the verification of their correctness.

In the industrial context correctness verification is usually performed by means of testing; the system is provided with input sequences drawn from a proper "coverage set" and its resulting behaviour is observed.

Due to the multiplicity of possibilities both for inputs to a system and originating from more and more use of parallelism and concurrency this approach turns out to be very costly and in any case it does not allow for the exhaustive verification of the correctness of the system. It allows only to detect errors which take place during the execution sequences used for the test.

In the last decade several theories have been developed which aim at coping with the problem of systems correctness by means of formal methodologies for the specification, design and verification of systems. These theories have been extended in order to deal with time, probability and stochastic aspects of behaviours.

Also real-time models where time is a dense quantity and verification can be done algorithmically (automatically) has been developed.

More recently, international standards for safety recommend the use of such methodologies, especially for critical systems.

Nevertheless, the use of formal methods in the industry is still quite limited. Apparently, major reasons for that are the notational difficulty of most formal methods available nowdays and the lack of integration between them. Notational complexity is often a deterrent to the use of formal methods stronger than the advantages of such methods. This is reinforced by the lack of models which support all the activities of system development:

1. requirements specification
2. validation of the specification
3. design
4. verification of the final product against the requirements

For each of the above activities different techniques have been developed independently. They are usually not at all integrated, neither compatible and quite often they have been tried only on toy-examples, bringing to results which are rather difficult to compare. Finally, most of the automatic tools developed for supporting the use of formal methods lack of industrial strength and so turn out to be unpractical when used in the industrial context.

---

3.      Objectives

The main objectives of the WG are:

1. To bring together scientists mainly of, but not only of, institutions within ERCIM, who are active in the field of formal methods and are willing to exchange their experience in the industrial usage of formal methods.
2. To coordinate efforts in the transfer of the formal methods technology and knowledge to the industry.
3. To promote research and development for the improvement of formal methods and tools with respect to their usage in the industry.

The above objectives will be met by means of:

1. Workshops where the participation of industrial professionals will be solicited.
2. Development projects with industrial partners.
3. Research projects and researchers mobility.

---

4.      Scientific Activities

1. FMICS 1996: 1st International Workshop on Formal Methods for Industrial Critical Systems
   St. Hugh's College, Oxford (UK), March 19, 1996
   
   
2. Special issue of the journal "Formal Methods in System Design"
   (Vol. 12, Nr. 2, March 1998)
   
   
3. FMICS 1997: 2nd International Workshop on Formal Methods for Industrial Critical Systems
   Cesena (Italy), July 4-5, 1997
   
   
4. Special issue of the journal "Formal Aspects of Computing"
   (Vol. 10, Nr. 4, 1998)

5. FMICS 1998: 3rd International Workshop on Formal Methods for Industrial Critical Systems
   Amsterdam (The Netherlands), May 25-26, 1998

6. Special issue of the journal "Formal Aspects of Computing"
   (Vol. 10, Nr. 5-6, 1998)

7. FMICS 1999: 4th International Workshop on Formal Methods for Industrial Critical Systems
   Trento (Italy), July 11-12, 1999

8. Special issue of the journal on "Science of Computer Programming"
   (Vol. 36, Issue 1, January 2000)

9. FMICS 2000: 5th International Workshop on Formal Methods for Industrial Critical Systems
   Berlin (Germany), April 3-4, 2000

10. Special issue of the journal "Formal Methods in System Design"
    (Vol. 19, Nr. 2, September 2001)

11. FMICS 2001: 6th International Workshop on Formal Methods for Industrial Critical Systems
    Paris (France), 16-17 July 2001

12. FMICS 2002: 7th International Workshop on Formal Methods for Industrial Critical Systems
    Málaga (Spain), 12-13 July 2002

13. Special issue of the journal on "Science of Computer Programming"
    (Vol. 46, Nr. 3, March 2003).

14. FMICS 2003: 8th International Workshop on Formal Methods for Industrial Critical Systems
    Trondheim (Norway), 5-7 July 2003

15. Special issue of the journal "Software Tools for Technology Transfer"
    (Vol. 5, Nr. 2-3, March 2004)

16. FMICS 2004: 9th International Workshop on Formal Methods for Industrial Critical Systems
    Linz (Austria), 20-21 September 2004

17. FMICS 2005: 10th International Workshop on Formal Methods for Industrial Critical Systems
    Lisbon (Portugal), 5-6 September 2005

18. FMICS 2006: 11th International Workshop on Formal Methods for Industrial Critical Systems
    Bonn (Germany), 26-27 August 2006 (LNCS Proceedings)

19. Special issue of the journal "Formal Methods in System Design"
    (Vol. 30, Nr. 3, June 2007)

20. FMICS 2007: 12th International Workshop on Formal Methods for Industrial Critical Systems
    Berlin (Germany), 1-2 July 2007 (LNCS Proceedings)

21. European project EC-MOAN
    2007-2009

22. FMICS 2008: 13th International Workshop on Formal Methods for Industrial Critical Systems
    L'Aquila (Italy), 15-16 September 2008 (LNCS Proceedings)

23. FMICS 2009: 14th International Workshop on Formal Methods for Industrial Critical Systems
    Eindhoven (The Netherlands), 2-3 November 2009 (LNCS Proceedings)

24. Special issue of the journal "Software Tools for Technology Transfer" (Vol. 11, Nr. 5, Nov. 2009)

25. FMICS 2010: 15th International Workshop on Formal Methods for Industrial Critical Systems
    Antwerp (Belgium), 20-21 September 2010 (LNCS Proceedings)

26. Special issue of the journal "Science of Computer Programming" (Vol. 76, Nr. 2, Feb. 2011)

27. FMICS 2011: 16th International Workshop on Formal Methods for Industrial Critical Systems
    Trento (Italy), 29-30 August 2011 (LNCS Proceedings)

28. FMICS 2012: 17th International Workshop on Formal Methods for Industrial Critical Systems
    Paris (France), 27-28 August 2012 (LNCS Proceedings)

29. European project SENSATION
    2012-2015

30. Formal Methods for Industrial Critical Systems: A Survey of Applications (Wiley, 2013)

31. Special issue of the journal "Science of Computer Programming" (Vol. 78, Nr. 7, Jul. 2013)

32. FMICS 2013: 18th International Workshop on Formal Methods for Industrial Critical Systems
    Madrid (Spain), 23-24 September 2013 (LNCS Proceedings)

33. Special issue of the journal "Science of Computer Programming" (Vol. 80(A), Feb. 2014)

34. FMICS 2014: 19th International Workshop on Formal Methods for Industrial Critical Systems
    Florence (Italy), 11-12 September 2014 (LNCS Proceedings)

35. Special issue of the journal "Software Tools for Technology Transfer" (Vol. 16, Nr. 6, Nov. 2014)

36. FMICS 2015: 20th International Workshop on Formal Methods for Industrial Critical Systems
    Oslo (Norway), 22-23 June 2015 (LNCS Proceedings)

37. Special issue of the journal "Science of Computer Programming" (Vol. 118, Mar. 2016)

38. FMICS-AVoCS 2016: Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems
    Pisa (Italy), 26-29 September 2016 (LNCS Proceedings)

39. FMICS-AVoCS 2017: Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems
    Torino (Italy), 18-20 September 2017 (LNCS Proceedings)

40. Special issue of the journal "Software Tools for Technology Transfer" (Vol. 20, Nr. 4, Aug. 2018)

41. FMICS 2018: 23rd International Conference on Formal Methods for Industrial Critical Systems
    Maynooth University (Ireland), 3-4 September 2018 (LNCS Proceedings)

42. FMICS 2019: 24th International Conference on Formal Methods for Industrial Critical Systems
    Amsterdam (The Netherlands), 30-31 August 2019 (LNCS Proceedings)

43. FMICS 2020: 25th International Conference on Formal Methods for Industrial Critical Systems
    Vienna (Austria), 2-3 September 2020 (LNCS Proceedings)

44. FMICS 2021: 26th International Conference on Formal Methods for Industrial Critical Systems
    Paris (France), August 24-26, 2021 (LNCS Proceedings)

45. FMICS 2022: 27th International Conference on Formal Methods for Industrial Critical Systems
    Warsaw (Poland), September 14-16, 2022 (LNCS Proceedings)

46. Special issue of the journal "Software Tools for Technology Transfer" (Vol. 24, Nr. 3, Aug. 2022)

47. Special issue of the journal "Software Tools for Technology Transfer" (Vol. 24, Nr. 6, Dec. 2022)

48. FMICS 2023: 28th International Conference on Formal Methods for Industrial Critical Systems
    Antwerp (Belgium), September 18-23, 2023 (LNCS Proceedings)

49. FMICS 2024: 29th International Conference on Formal Methods for Industrial Critical Systems
    Milan (Italy), September 9-11, 2024 (LNCS Proceedings)

50. FMICS 2025: 30th International Conference on Formal Methods for Industrial Critical Systems
    Aarhus (Denmark), August 27-28, 2025 (LNCS Proceedings)

---

5.      Best Paper Awards

• FMICS-AVOCS 2017 best papers
  • Etienne André.
    A unified formalism for monoprocessor schedulability analysis under uncertainty
  • Rutger van Beusekom, Jan Friso Groote, Paul Hoogendijk, Rob Howe, Wieger Wesselink, Rob Wieringa, and Tim Willemse
    Formalising the Dezyne Modelling Language in mCRL2

• FMICS 2018 best paper
       Maarten Bartholomeus, Bas Luttik, and Tim Willemse
       Modelling and Analysing ERTMS Hybrid Level 3 with the mCRL2 Toolset

• FMICS 2019 best paper
       Matthias Volk, Norman Weik, Joost-Pieter Katoen, and Nils Nielssen
       A DFT Modeling Approach for Infrastructure Reliability Analysis of Railway Station Areas

• FMICS 2020 best paper
       Rong Gu, Eduard Enoiu, Cristina Seceleanu, and Kristina Lundqvist
       Verifiable and Scalable Mission-Plan Synthesis for Multiple Autonomous Agents

• FMICS 2021 best paper
       Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marcé, David Mentré, and Hiroaki Inoue
       Automated Verification of Temporal Properties of Ladder Programs

• FMICS 2022 best paper
       Franck Cassez, Joanne Fuller and Horacio Mijail Anton Quiles
       Deductive Verification of Smart Contracts with Dafny

• FMICS 2023 best paper
       Djurre van der Wal, Marcus Gerhold, and Mariëlle Stoelinga
       Conformance in the Railway Industry: Single-Input-Change Testing a EULYNX Controller

• FMICS 2024 best papers
  • Jan Steffen Becker
    Safe Linear Encoding of Vehicle Dynamics for the Instantiation of Abstract Scenarios
  • Robby, John Hatcliff, and Jason Belt
    Logika: The Sireum Verification Framework

• FMICS 2025 best paper
       Stefan Hallerstede, Robby, John Hatcliff, Jason Belt, and David Hardin
       Proof Engineering in Logika: Synergistically Integrating Automated and Semi-automated Program Verification

---

6.      Official ERCIM Documents about FMICS

• Memorandum of Understanding for ERCIM working groups - August 1996
• Updated Memorandum of Understanding for ERCIM working groups - May 2001
• ERCIM News No. 25 - April 1996
  report by Diego Latella and Stefania Gnesi
• ERCIM News No. 26 - July 1996
  report by Diego Latella
• ERCIM News No. 31 - October 1997
  report by Stefania Gnesi and Diego Latella
• ERCIM News No. 34 - July 1998
  report by Diego Latella
• ERCIM News No. 39 - October 1999
  Towards Reliable Computer Systems?
  by Diego Latella, Stefania Gnesi, and Hubert Garavel
• ERCIM News No. 47 - October 2001
  report by Hubert Garavel
• ERCIM News No. 47 - October 2001
  How can I be sure that my DVD player understands my TV?
  by Wan Fokkink, Izak van Langevelde, Bas Luttik and Yaroslav Usenko
• ERCIM News No. 54 - July 2003
  report by Thomas Arts and Wan Fokkink
• FMICS receives the ERCIM Working Group Award 2003
• ERCIM News No. 60 - January 2005
  report by Juan Bicarregui, Andrew Butterfield and Alvaro Arenas
• ERCIM News No. 77 - April 2009
  report by Alessandro Fantechi
• ERCIM News No. 91 - October 2012
  report by Radu Mateescu
• ERCIM News No. 92 - January 2013
  report by Alessandro Fantechi, Francesco Flammini, and Stefania Gnesi
• ERCIM News No. 108 - January 2017
  report by Maurice ter Beek
• ERCIM News No. 112 - January 2018
  report by Ana Cavalcanti, Laure Petrucci, and Cristina Seceleanu
• ERCIM News No. 123 - October 2020
  report by Maurice ter Beek
• ERCIM News No. 127 - July 2021
  report by Maurice ter Beek
• ERCIM News No. 131 - October 2022
  report by Maurice ter Beek
• ERCIM News No. 135 - October 2023
  report by Maurice ter Beek
• ERCIM News No. 139 - October 2024
  report by Maurice ter Beek

---

7.      Contacts

As of October 2022, the FMICS Working Group is being chaired by:
 

Maurice ter Beek

FMT lab - ISTI-CNR

Pisa (Italy)

The FMICS Chair is assisted by the FMICS Board, the members of which are:

• Alessandro Fantechi (Univ. of Firenze)
• Hubert Garavel (INRIA): Dissemination and Web site
• Tiziana Margaria (CSIS, Univ. of Limerick, and LERO)
• Radu Mateescu (INRIA)
• Jaco van de Pol (Aarhus University and University of Twente)

The former FMICS Chairs are:

• Diego Latella (August 1996 - July 1999)
• Hubert Garavel (July 1999 - July 2002)
• Stefania Gnesi (July 2002 - November 2005)
• Pedro Merino (November 2005 - October 2008)
• Alessandro Fantechi (November 2008 - October 2011)
• Radu Mateescu (November 2011 - October 2014)
• Tiziana Margaria (November 2014 - November 2018)
• Jaco van de Pol (November 2018 - October 2022)

The former FMICS Board Members are:

• Alvaro Arenas (STFC, 2007)
• Pedro Merino (University of Malaga, until November 2017)
• Lubos Brim (CRCIM, until July 2018)
• Stefania Gnesi (ISTI-CNR, until August 2020)
• Diego Latella (ISTI-CNR, until August 2020)

As of September 2020, the working group initiators are now Honorary Members of FMICS:

• Stefania Gnesi (ISTI-CNR)
• Diego Latella (ISTI-CNR)

---

8.      Institutions and Participants

A legacy web page listing the FMICS members and institutions is available here. At present, participation to the FMICS working group essentially takes place by attending the annual FMICS conference.

---