Formal Methods Teaching Committee

The aim of the FME Teaching Committee is to support a worldwide improvement in learning formal methods, mainly by teaching but also via self-learning.

Events & Meetings

We organise events and meetings.

Courses Database

We maintain a database of FM courses.

Case Studies

We maintain a list of FM case studies.

Curriculum

On Education: Forthcoming Special Issue of ACM’s Formal Aspects of Computing journal (Scroll down for links to the papers)

ACM has been publishing guidelines for computer technology university curricula for more than five decades, with the first one specifically for Computer Science published in 2001. To the best of our knowledge, these are the only curricular guidelines that have worldwide recognition. While it is likely that no university follows them to the letter, they are enormously valuable as a reference point. Since the field of computer technology evolves quickly, ACM regularly updates its guidelines on what should be taught. For instance, the Computer Science curricular guidelines are revised once every decade; CS2023 is the latest revision, recently published.

The ACM teaching recommendation model is complex. A short overview is that it contains 17 knowledge areas deemed essential for Computer Science, each such area further divided into knowledge units made of topics, some mandatory to teach and some elective.

The papers in this issue put forward views as to why and how Formal Methods should be represented in Computer Science curricula, in some cases, just as suggested in the ACM guidelines, but in other cases, providing different guidance. The starting point is the questions below, which have arisen from informal discussions with CS2023 contributors to various knowledge areas.

  • Does every Computer Scientist need to know Formal Methods?

Discussions here centred around the view that, while there is a belief that formal methods are important, and they are growing in importance, it may not yet be clear that every Computer Science graduate will need to use a formal method in their career.

  • Are Formal Methods just for the safety-critical industry?

Here, the issue under consideration was not the importance of Formal Methods, but that it might be restricted to a number of industry segments.

  • Is the current offer of Formal Methods education adequate?

The point debated here was whether Formal Methods should (continue to) be covered at graduate level as an elective rather than a required subject. Given (the perception) that few undergraduate programs teach Formal Methods, the discussion was whether we can conclude that the guidelines for the Foundations of Programming Languages and Software Engineering knowledge areas capture the current curriculum landscape, and so are appropriate.

Each paper included in this special issue addresses one of the questions above.

In Broy et al, arguments are given that every Computer Scientist needs to know the theoretical background of their field. An analogy is given to database management: “Just as not all graduates will need to know how to work with databases either, it is still important for students to have a basic understanding of how data is stored and managed efficiently.'' Their message brings out the fact that Computer Science graduates are also (software and systems) engineers. And it is perhaps uncontroversial that “No engineer should be ignorant of the foundations of their subject and the formal methods based on these.''

In ter Beek at al, an extensive review of industrial uses of Formal Methods is presented, demonstrating that safety-critical systems are not the only beneficiaries of precision, reasoning, and proof. The authors “… present a broad scope of successful applications of formal methods in industry, not limited to the well-known success stories from the safety-critical domain”. For example, they present use cases in lithography manufacturing and cloud security in e-commerce, and industrial use in Europe, Asia, and North and South America.

In Dongol at al, the authors explain that Formal Methods are currently not taught well, being often associated with logic and theory. They argue that we need to teach all Computer Science students “Formal Methods thinking'', which they define as the ideas from Formal Methods applied in “informal, lightweight, practical and accessible ways''. This includes, for instance, understanding key concepts, but applying them using natural languages. The authors argue that Formal Methods thinking should be part of the recommended curriculum for every Computer Science student, since students then become much better programmers.

A one-page summary of the contributions of the papers appears in the CS2023 curricular guidelines on page 433.

The 35 authors of these papers are well-known computer scientists who have extensive experience in teaching Formal Methods in Academia or working with them in Industry. They argue for introducing Formal Methods as a knowledge area in the ACM guidelines, since currently Formal Methods are covered only as elective topics in some knowledge units in two distinct knowledge areas: Foundations of Programming Languages and Software Engineering.

Formal Methods are supported nowadays by efficient software tools; this is a game changer regarding their usability and adoption from students and practitioners. The evidence put forward in the papers of this special issue suggests that not indicating Formal Methods as a core domain in a Computer Science curriculum in 2024 is incomprehensible, similar maybe to how Artificial Intelligence was not included just 10 years ago in the 2013 guidelines.

(Luigia Petre, Åbo Akademi University, Finland and Ana Cavalcanti, University of York, UK)

Papers in the Special Issue

Objectives

Our objectives are:

  1. To revive bring up-to-date an old database of formal methods courses taught worldwide. We plan to review this database yearly. The current FM course repository is available online. You can contribute courses using the form below.

  2. To setup a repository of formal methods case studies, containing simpler as well as more complex examples of using formal methods. This can be liken to the Github repository for software or the Biomodels database for computational models of biological processes. The simpler examples can be for instance used in teaching, while the more complex for (self-)learning various formal methods and for demonstrating the formal methods strength to, for instance, industry.

  3. To setup a secured repository of exam exercises for formal method courses. These will be available only to teachers.

  4. To work towards achieving a BoK (Body of Knowledge) in Formal Methods, that can enable self-learning as well as various future certifications in Formal Methods. This objective will start up from earlier efforts in this direction.

  5. To setup a list of “summer” schools in Formal Methods.

In the long run, we have the following goals:

  1. We plan to coordinate “providers” and “consumers” of Formal Methods, so that when some researcher or industrial partner needs certain knowledge in Formal Methods, we can advice where to address these needs.

  2. We plan to investigate whether certain degrees in Formal Methods are feasible. We aim to see whether an International MSc program in Formal Methods can be organised, for instance.

  3. We plan to make industry and life sciences beneficiaries of Formal Methods, by providing case studies from Academia to Industry/Science to demonstrate potential and by getting interesting/real life problems to analyse from Industry/Science to Academia.

FM Courses

Our searchable database of formal methods courses is available online. You can use the form below to add a new course.

Submit a new course

Once you submit your course, an external Github page will open. To confirm your submission, click the button Submit new issue.

If you can’t find a concept or tool in the list below, you can manually add them after submission, using the Github interface.

  • Abstract Interpretation
  • Coq

Members

The committee has members from all over the world:

We also keep a list of previous members.

Meetings