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:

The lecture notes of the course are on Clemens’ webpage.