Formal Methods for System Design

First semester

The whole course is worth 12 ECTS, and takes place over two semesters (120 hours in total). During the first semester, we focus on the foundations of model checking and synthesis. My notes are heavily inspired by the wonderful book Principles of Model Checking by Baier & Katoen. The topics I cover are as follow:

• Full course outline. [PDF]
• Chapter 1: Formal verification. [Slides]
• Chapter 2: Modeling systems. [Slides]
• Chapter 3: Linear temporal logic. [Slides]
• Chapter 4: Computation tree logic. [Slides]
• Chapter 5: Symbolic model checking. [Slides]
• Chapter 6: Model checking probabilistic systems. [Slides]
• Chapter 7: Synthesis through game theory.

There are no slides for Chapter 7: I use a flipped classroom approach, focusing on a chapter of the Handbook of Model Checking. Students read the chapter in autonomy and we discuss it together.

During the first semester, students also learn to use model checking and verification tools such as SPIN, Uppaal, Storm or Prism.

Second semester

There are no classical lectures during the second semester. Two activities take place in parallel.

First, students prepare and give lectures on an advanced topic of their choice, helped in their preparation by the teaching team. We obviously focus on the understanding of the subject, but also stress on the pedagogical quality of the lectures.

Second, students take part in a semester-long project mixing AI (reinforcement learning in particular) and formal methods. The ecosystem of choice is Gymnasium, a standard API for RL that essentially offers a playground to synthesize and assess controllers in various environments. We coach the students through regular meetings (roughly every ten days) where they present their progress, their difficulties, etc. We start by exploring classical methods in RL and model checking and reach advanced techniques (and difficult environments, such as the Lunar Lander below) by the end of the semester.