Lecture “Model Checking”
Lecture “Model Checking”
Lehrveranstaltung mit SWS 4/4/0 (Vorlesung/Übung/Praktikum) im WS 2025
Dozent
Umfang (SWS)
- 4/4/0
Sprache
- auf Englisch
Module
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 3.
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 16)
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).
Creditability
Bachelor Informatik (PO 2009)
Bachelor Informatik (PO 2025)
- INF-25-Ma-FTK-MC: exam according to module description
Master Informatik (PO 2010)
Master Computer Science (PO 2025)
- INF-25-Ma-FTK-MC: exam according to module description
Diplom Informatik (PO 2010)
Diplom Informatik (PO 2025)
- INF-25-Ma-FTK-MC: exam according to module description
Master Computational Logic
- MCL-TCSL: exam according to module description
Master Computational Modeling and Simulation
- CMS-LM-ADV: oral exam (30 minutes)
- CMS-LM-AI: oral exam (30 minutes)
- CMS-LM-MOC: oral exam (30 minutes)
Oral Exams
Appointments for the oral examination are to be made via our secretary's office. Please contact Andrea Kühn via e-mail.
Contact
In case of organisational questions, please contact Sascha Klüppelholz.
