Emilio's web page

Model Checking

Academic year 2023/24

Lecturers: Clemens Grabmayer and Emilio Tuosto

This course introduces to the formal modelling and verification through classical model checking approaches. The course poses particular emphasis on the so-called reactive systems, which embrace a wide range of modern distributed and communicating systems. The main topics of the course are temporal logics (specifically LTL, CTL, and CTL*), safety and liveness properties of reactive systems as well as fairness conditions. Some basic model checking algorithms are presented and their application to realistic scenarios is analysed.

References and material

Baier, Katoen: Principles of model checking. MIT Press
Clarke, Grunberg, Peled: Model checking. MIT Press
Click here for the recent research paper on model checking discussed in the last lecture

Lecture notes:

12/02/24: First lecture: overview and motivations, counter.py
13/02/24: Second lecture: transition systems and temporal properties
19/02/24: Third lecture: Invariance, safety, liveness, and fairness
21/02/24: Fourth lecture: LTL syntax, semantics, and exercises (pages 1-4)
22/02/24: Fift lecture: Model checking LTL with Büchi automata and LTL fairness formulae (pages 6-12)
06/03/24: Sixt lecture: CTL
07/03/24: Seventh lecture: CTL+ and CTL* (pages 6-9)
07/03/24: Research paper on model checking