Model Checking

Prof. Dr. Christel Baier and Dr. Sascha Klüppelholz
SWS: (4/4/0), in English

Description

Model Checking is a fully automatic verification method for reactive systems. This course provides an introduction to the main principles of model checking:

• modeling reactive systems by means of transition systems
• linear-time properties and Büchi automata
• linear temporal logic and automata-based model checking
• computation tree logic
• abstraction ((bi)simulation)
• probabilistic model checking

Literature

The course follows the book “Principles of Model Checking” (C. Baier, J.P. Katoen, Principles of Model Checking, MIT Press) closely. This book is available at the SLUB (Lehrbuchsammlung).

Registration

Enrolling via OPAL is required.

Dates

There is no fixed assignment of the lectures and exercises to time slots. It will be announced each week when lectures and exercises will take place in the following week. The first lecture will take place on October 17, 2024, at 09:20 am.

The course consists of a (4/2/0) lecture with exercises for the theoretical foundations and an introduction to model checkers with practical exercises (0/2/0).

Prerequisites

For the course, basic knowledge on algorithms, complexity theory, automata theory and logic is presumed.

Exam and Creditability

Bachelor Informatik

• INF-B-510: Vertiefung in der Informatik (30 minute oral exam)
• INF-B-520: Spezialisierung in der Informatik (30 minute oral exam)

Master Informatik

• INF-BAS6: Basismodul Theoretische Informatik (exam according to module description)
• INF-VERT6: Vertiefungsmodul Theoretische Informatik (exam according to module description)

Diplom Informatik

• INF-BAS6: Basismodul Theoretische Informatik (exam according to module description)
• INF-VERT6: Vertiefungsmodul Theoretische Informatik (exam according to module description)

Master Computational Logic

• MCL-TCSL: Theoretical Computer Science and Logic (exam according to module description)

Master Computational Modeling and Simulation

• CMS-LM-MOC: Models of Computation (30 minute oral exam)
• CMS-LM-ADV: Advanced Logical Modeling (30 minute oral exam)

Contact