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 der Veranstaltung Model Checking haben wir die theoretischen Grundlagen des Model Checkings kennen gelernt. Insbesondere haben wir die Spezifikationssprachen LTL und CTL eingefĂŒhrt, ihre AusdrucksstĂ€rke untersucht, und die wichtigsten algorithmischen AnsĂ€tze fĂŒr das Model Checking erarbeitet.
In diesem Seminar wollen wir uns mit weiterfĂŒhrenden, aktuellen Themen im Bereich Model Checking beschĂ€ftigen.
Einstiegsliteratur fĂŒr dieses Seminar ist neben Originalarbeiten:
- Â Edmund M Clarke, Thomas A Henzinger, Helmut Veith, and Roderick Bloem. Handbook of model checking, volume 10. Springer, 2018
Voraussetzungen:
- Â Veranstaltung "Model Checking" und/oder "Logik in der Informatik"
- Kursleiter/in: Thomas Zeume