Vorlesung „Model Checking“
Vorlesung „Model Checking“
Lehrveranstaltung mit SWS 4/4/0 (Vorlesung/Übung/Praktikum) im WS 2026
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.
Literatur
Die Vorlesung folgt dem Buch „Principles of Model Checking“ (C. Baier, J.P. Katoen; Principles of Model Checking; MIT Press). Dieses ist in der SLUB (Lehrbuchsammlung) verfügbar.
Anmeldung
Für die Teilnahme ist eine Registrierung via Opal bis zum 2. November erforderlich.
Voraussetzungen
Es werden Grundkenntnisse in Algorithmen, Komplexitätstheorie, Automatentheorie und Logik vorausgesetzt.
Termine
Donnerstag und Freitag, 9:20–10:50 und 11:10–12:40, APB E005 (Beginn: 15. Oktober)
Vorlesung und Übung sind den genannten Terminen nicht fest zugeordnet. Es wird wöchentlich, jeweils für die Folgewoche, mitgeteilt, wann die Vorlesung und wann Übungen stattfinden.
Die Lehrveranstaltung umfasst eine (4/2/0) Vorlesung mit Übungen zu den theoretischen Grundlagen sowie eine Einführung in Model Checker mit praktischen Übungen (0/2/0).
Prüfungsleistung
Bachelor Informatik (PO 2025)
- INF-25-Ma-FTK-MC: 30-minütige mündliche Prüfung
Master Computer Science (PO 2025)
- INF-25-Ma-FTK-MC: 30-minütige mündliche Prüfung
Diplom Informatik (PO 2025)
- INF-25-Ma-FTK-MC: 30-minütige mündliche Prüfung
Gemäß Modulbeschreibung besteht die Modulprüfung aus einer nicht öffentlichen mündlichen Einzelprüfung von 30 Minuten Dauer. Die möglichen Prüfungstermine werden gegen Ende des Semesters in der Vorlesung bekannt gegeben. Um Ihren individuellen Prüfungstermin zu vereinbaren, kontaktieren Sie bitte die Sekretärin des Lehrstuhls, Andrea Kühn, per E-Mail.
Kontakt
Bei organisatorischen Fragen wenden Sie sich bitte an Sascha Klüppelholz.
