Automatische Software Verifikation (ASV)

Die integrierte Veranstaltung befasst sich mit dem Techniken zur automatischen Softwareverifikation. Die konkreten Inhalte entnehmen Sie bitte den Lehrinhalten und -zielen.

Termine im SS2022

13.04., 19.04., 20.04. online via Zoom (Zugangsdaten im Moodle Kurs)

Di 11:45-13:15, S2|02 C120
Mi 13:30-15:00, S2|02 C110

Die Veranstaltung findet in der Regel jedes Sommersemester statt und wird über die Lernplattform Moodle organisiert.

Lerninhalte und -ziele

Die Veranstaltung befasst sich mit dem Techniken zur automatischen Softwareverifikation und behandelt dabei folgende Themenbereiche:

  • operationelle Semantik von sequentiellen Programmen
  • konfigurierbare Programmanalyse inklusive Konfiguration für Datenflussanalysen und Model Checking
  • counterexample-guided abstraction refinement (CEGAR)
  • Bounded Model Checking
  • k-Induktion
  • kooperative Verifikation, insbesondere Conditional Model Checking

Nach erfolgreicher Teilnahme an der Veranstaltung können die Studierenden eine Vielzahl von Verfahren zur automatischen Verifikation benennen. Sie können die den Verfahren zugrunde liegenden Formalismen wiedergeben, die Funktionsweise der Verfahren beschreiben und die Verfahren klassifizieren. Außerdem können die Studierenden die Verfahren auf Beispielen anwenden und neue konfigurierbare Programmanalysen entwickeln.

Empfohlene Vorkenntnisse

Informatikkenntnisse entsprechend der ersten vier Semester des Bachelorstudiengangs Informatik, insbesondere Kenntnisse aus der Vorlesung Aussagen und Prädikatenlogik oder Vergleichbares

Literaturempfehlungen

Semantik

  • K. R. Apt, F. S. de Boer, E.-R. Olderog: Verification of Sequential and Concurrent Programs. Springer 2009.
  • Edsger W. Dijkstra: A Discipline of Programming, Prentice-Hall, 1976.

Domänen, Programmanalyse, Model Checking, CEGAR

  • E. M. Clarke, T.A. Henzinger, H. Veith, R. Bloem: Handbook of Model Checking, Springer, 2018.
  • D. Beyer D., T. A. Henzinger, G. Théoduloz G.: Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis, CAV, LNCS 4590, pp. 504-518, Springer, 2007.
  • Ranjit Jhala and Rupak Majumdar. Software model checking. ACM Comput. Surv. 41, 4, Article 21, 2009.
  • D. Beyer, S. Löwe: Explicit-State Software Model Checking Based on CEGAR and Interpolation, FASE, LNCS 7793, pp. 146-162, Springer, 2013.
  • F. Nielson, H. R. Nielson, C. Hankin. Principles of Program Analysis, Springer, 2009.
  • T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre: Lazy abstraction, POPL, pp. 58-70, ACM, 2002.
  • D. Beyer, S. Löwe, P. Wendler: Sliced Path Prefixes: An Effective Method to Enable Refinement Selection, FORTE, LNCS 9039, pp. 228-243, Springer, 2015.
  • D. Beyer, A. Cimatti, A. Griggio, M. E. Keremoglu, R. Sebastiani: Software model checking via large-block encoding, FMCAD, pp. 25-32, IEEE, 2009.
  • M. Heizmann , J. Hoenicke, A. Podelski: Refinement of Trace Abstraction, SAS, LNCS 5673, pp. 69-85, Springer, 2009.

Bounded Model Checking, k-Induktion

  • A. Biere, A. Cimatti, E. Clarke, O. Strichman, Y. Zhu: Bounded model checking, Advances in computers 58 (11), Academic Press, 2003.
  • E. Clarke, D. Kroening, K. Yorav: Behavioral consistency of C and Verilog programs using bounded model checking, DAC, pp. 368-371, ACM, 2003.
  • A. F. Donaldson, L. Haller, D. Kroening, P. Rümmer: Software Verification Using k-Induction, SAS, LNCS 6887, pp. 351-368, Springer, 2011.

Conditional Model Checking

  • D. Beyer, T. A. Henzinger, M. Erkan Keremoglu, P. Wendler: Conditional model checking: a technique to pass information between verifiers, FSE, ACM, 2012.
  • D. Beyer, M.-C. Jakobs, T. Lemberger, H. Wehrheim: Reducer-based construction of conditional verifiers, ICSE, pp. 1182-1193, ACM, 2018.