Lecture “Model Checking”
Lecture “Model Checking”
Course with SWS 4/4/0 (lecture/exercise/practical) in WS 2026
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
Registration via Opal is required until November 2.
Prerequisites
For the course, basic knowledge on algorithms, complexity theory, automata theory and logic is presumed.
Dates
Thursdays and Fridays, 9:20–10:50 and 11:10–12:40, APB E005 (starting October 15)
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 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).
Examination
Bachelor Informatik (PO 2025)
- INF-25-Ma-FTK-MC: 30-minute oral exam
Master Computer Science (PO 2025)
- INF-25-Ma-FTK-MC: 30-minute oral exam
Diplom Informatik (PO 2025)
- INF-25-Ma-FTK-MC: 30-minute oral exam
According to the module description, the exam is a non-public individual oral examination lasting 30 minutes. Potential exam dates will be announced towards the end of the semester. The individual exam appointments can then be arranged by e-mailing our secretary, Andrea Kühn.
Contact
In case of organizational questions, please contact Sascha Klüppelholz.
