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