Das Thema baut auf einem Überblick in [1] auf. Hier soll neben einer Erklärung der grundlegenden Ansätze von Model Checking [2] und deduktive Verifikation [3] ein Überblick gegeben werden, auf welche Arten man die beiden Ansätze verbinden kann (bspw. Abstract Interpretation, Symbolic Model Checking, Predicate Abstraction, Symbolic Execution, Bounded Model Checking and k-Induction, Interpolation-Based Model Checking, Conflict-Driven Reachability).
In Absprache mit dem Betreuer soll hierbei nach Wahl der/des Seminarteilnehmenden exemplarisch eine dieser Arten vertieft werden.

1. Shankar, N.: Combining Model Checking and Deduction (Handbook of Model Checking, Springer 2018, Paper)
2. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking (MIT Press, Cambridge 1999, Paper)
3. Shankar, N.: Automated Deduction for Verification (ACM Comput. Surv. 41(4), 20:1–20:56, 2009, Paper)