Home  |  Impressum  |  Datenschutz  |  Sitemap  |  KIT

Thema 2: Combining Model Checking and Deduction

Combining Model Checking and Deduction
Typ: Seminarthema SS 2020
Betreuer:

Michael Kirsten

Links: Paper

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)