Wie kann die Korrektheit von Software und Hardware formal überprüft werden? Im Model Checking werden Software- und Hardware-Module durch Transitionssysteme formalisiert; gewünschte Eigenschaften mit Hilfe logischer Formalismen formal beschrieben; und mit Hilfe von Algorithmen automatisiert überprüft, ob ein Transitionssystem eine formal spezifizierte Eigenschaft besitzt.
In dieser Veranstaltung werden die theoretischen Grundlagen des Model Checkings vermittelt, mit einem Fokus auf logik-basierten Spezifikationssprachen. Die Spezifikationssprachen LTL und CTL werden eingeführt, ihre Ausdrucksstärke untersucht, und die wichtigsten algorithmischen Ansätze für das Model Checking vorgestellt.
Einstiegsliteratur für diese Veranstaltung sind die Bücher:
* Baier, Christel, and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008.
* Clarke Jr, E. M., Grumberg, O., Kroening, D., Peled, D., & Veith, H. Model checking. MIT press. 2018.
Voraussetzungen:
* Erfolgreicher Besuch der Grundlagenvorlesungen Mathematik
* Erfolgreicher Besuch der Veranstaltung "Theoretische Informatik"
* Hilfreich: Logik in der Informatik, Datenstrukturen und elementare Programmierkenntnisse
- Kursleiter/in: Felix Tschirbs
- Kursleiter/in: Thomas Zeume