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)