Formal Methods Teaching Committee

FMTea tutorial series

FME’s Teaching Committee coordinates a tutorial series, planned to be held monthly. It aims to increase the awareness and sharing of tools and techniques used for teaching formal methods. The series is held online via zoom. More information here.

2023

  • June 16, 2023, 3 pm CEST: Prof Laura Kovács, Vienna University of Technology (TU Wien), Austria: Teaching Formal Reasoning at TU Wien.
  • May 26, 2023, 3 pm CEST: Research Director Thierry Lecomte, ClearSy, France: Teaching and Training in Formalisation with B. The recording of Dr. Lecomte’s lecture can be seen here.
  • April 28, 3 pm CEST: Associate Prof Stefan Hallerstede (Aarhus University, Denmark): A guide to Not teaching Formal Methods. The recording of Prof. Hallerstede’s lecture can be seen here.
  • March 31, 3 pm CEST: Associate Prof Emil Sekerinski (McMaster University, Canada): Teaching Concurrent Programming. The recording of Prof. Sekerinski’s lecture can be seen here.

2022

  • December 9, 2022, 3 pm CET: Principal Research Engineer Markus A. Kuppe, (RiSE group at Microsoft Research, US): Stories from the trenches: Teaching the TLA+ specification language in Industry. The recording of Eng. Kuppe’s lecture can be seen here.
  • October 28, 2022, 3 pm CET: Dr Allan Blanchard (CEA-LIST, France): Formal methods for beginners and for C programs - Using Frama-C and its WP plug-in for teaching. The recording of Dr. Blanchard’s lecture can be seen here.
  • September 30, 2022, 3 pm CEST: Prof Michael Leuschel (Heinrich-Heine-University Düsseldorf, Germany): Teaching Formal Methods and Theoretical Computer Science with ProB. The recording of Prof Leuschel’s lecture can be seen here.
  • August 26, 2022, 3 pm CET: Dr Robert Lewis (Brown University, US): Teaching the theory and practice of proof assistants with Lean. The recording of Dr. Lewis’ lecture can be seen here.
  • July 29, 2022: Prof Erika Abraham (RWTH Aachen University, Germany). The recording of Prof. Abraham’s lecture can be seen here.
  • June 17, 2022: Dr Tim Nelson (Brown University, US): Building Formal Methods Classes for Everybody. The recording of Dr Nelson’s lecture can be seen here.
  • April 28, 2022, 3 pm CET: Prof. Jeremy Gibbons (University of Oxford, UK): How to Design Co−Programs. The recording of Prof. Gibbons’s lecture can be seen here.
  • February 25, 2022, 3 pm CET: Prof Shriram Krishnamurthi (Brown University, US): From Tests to Properties: Property-Based Testing Using Relational Problems. The recording of Prof. Krishnamurthi’s lecture can be seen here.

2021

  • December 10,2021: Assoc Prof David Pearce (Victoria University of Wellington, New Zealand): Teaching Software Verification with Whiley. The recording of Assoc. Prof. Pearce’s lecture can be seen here.
  • November 20-21, 9am-4pm CET: Tutorials @ FM2021
  • October 29, 2021, 3pm CET: Dr Ran Ettinger (Ben-Gurion University, Israel): Teaching Cantor’s theorem, a pumping lemma, and the derivation of a heapsort algorithm using Dafny. The recording of Dr. Ettinger’s lecture can be seen here.
  • September 24, 2021, 3pm CET: Prof Sandrine Blazy (University of Rennes 1, France): Why3 tool for deductive program verification. The recording of Prof. Blazy’s lecture can be seen here.

Contribute

You can contribute course information using this form: https://fme-teaching.github.io/#fm-courses.

Aim

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.

Members

Objectives

  1. We revive and bring up-to-date an old database of formal methods courses (http://www4.di.uminho.pt/FME-SoE/resources.html) taught worldwide. We plan to review this database yearly.
    The current FM course repository is located here: https://fme-teaching.github.io/courses/.
    You can contribute courses using this form: https://fme-teaching.github.io/#fm-courses.
  2. We 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. We setup a secured repository of exam exercises for formal method courses. These will be available only to teachers.
  4. We work towards achieving a BoK (Body of Knowledge) in Formal Methods, that would enable self-learning as well as various future certifications in Formal Methods. This objective will start up from earlier efforts in this direction, see http://formalmethods.wikia.com/wiki/FMBoK.
  5. We 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.

Web site

We are using the following page for information about FME’s Teaching Committee:
https://fme-teaching.github.io/

Contact

Please contact us if you would like to contribute to any of these initiatives: teaching@fmeurope.org

Share