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:
- Grundlagenvorlesungen Mathematik
- EinfĂŒhrung in die Theoretische Informatik (ggf. kann das nötige Wissen auch nachgeholt werden)
- Hilfreich: Logik in der Informatik, Datenstrukturen und elementare Programmierkenntnisse
- Kursleiter/in: Thomas Zeume