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.
Eine mögliche Liste von Themen ist unten aufgefĂŒhrt. Die Vorstellung anderer Themen ist nach Absprache möglich.
Mögliche Themen
- Aus "Edmund M Clarke, Thomas A Henzinger, Helmut Veith, and Roderick Bloem. Handbook of model checking, volume 10. Springer, 2018"
- Chapter 6: Partial-Order Reduction
- Chapter 11: Satisfiability Modulo Theories
- Chapter 12: Compositional Reasoning
- Chapter 14: Interpolation and Model Checking
- Chapter 15: Predicate Abstraction for Program Verification
- Chapter 16: Combining Model Checking and Data-Flow Analysis
- Chapter 17: Model Checking Procedural Programs
- Chapter 19: Combining Model Checking and Testing
- Chapter 20: Combining Model Checking and Deduction
- Chapter 21: Model Checking Parameterized Systems
- Chapter 22: Model Checking Security Protocols
- Chapter 26: The mu-calculus and Model Checking
- Chapter 28: Model Checking Probabilistic Systems
- Model Checking und Lernen: Rajarshi Roy, Dana Fisman, Daniel Neider: Learning Interpretable Models in the Property Specification Language. IJCAI 2020: 2213-2219
- Hana Chockler, Joseph Y. Halpern, Orna Kupferman: What causes a system to satisfy a specification?. ACM Trans. Comput. Log. 9(3): 20:1-20:26 (2008)
- Kursleiter/in: Thomas Zeume