Thema 8: Predicate Abstraction for Program Verification

Predicate Abstraction for Program Verification
Typ: Seminarthema WS 2020/21
Betreuer:

Michael Kirsten

Links: Paper

Das Thema baut auf einem Überblick in [1] auf. Im Kontext der Programmverifikation wird die Technik in [2] weiter eingeordnet. Hier sollen neben einer Erklärung der grundlegenden Problemstellung sowohl die zugrundeliegenden Algorithmen und Techniken vorgestellt werden als auch auf die Verwendung innerhalb der CEGAR-Technik [3] eingegangen werden.
Des Weiteren soll innerhalb des Seminars in Absprache mit dem Betreuer nach Wahl der/des Seminarteilnehmenden auf die Funktionsweise und Verwendung von "Predicate Abstraction" in zumindest einem praktischen Werkzeug eingegangen werden (siehe hierzu insbesondere Abschnitt 15.8 in [1]).

  1. Jhala, R., Podelski, A., Rybalchenko, A.: Predicate Abstraction for Program Verification - Safety and Termination
    (Handbook of Model Checking, Springer 2018, Paper)
  2. Jhala, R., Majumdar, R.: Software Model Checking (ACM Comput. Surv. 41(4), 21:1–21:54, 2009, Paper)
  3. Clarke, E.M., Kurshan, R.P., Veith, H.: The Localization Reduction and Counterexample-Guided Abstraction Refinement
    (Essays in Memory of Amir Pnueli 2010, Springer 2010, Paper)