Automatische Softwareverifikation

Automatische Software Verifikation (ASV)

Dozentin: Prof. Dr. Marie-Christine Jakobs

Die Veranstaltung findet in der Regel jedes Sommersemester statt.

Aktuelle Veranstaltungsinformation

Bis mindestens einschließlich 31.05.2020 findet die Veranstaltung lediglich online statt. Details erfahren Sie in Moodle.

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

Klausureinsicht

Die Klausureinsicht findet am 09.09.2020 – 14:00-15:00Uhr in S101/A03 statt.

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
  • counter-example guided abstraction refinement (CEGAR)
  • Bounded Model Checking
  • k-Induktion
  • kooperative Verifikation, insbesondere Conditional Model Checking
  • inkrementelle Verifikation
  • Nachprüfung von Verifikationsergebnissen (a la Proof-Carrying Code, Witness Validation)
  • Generierung von Testeingaben mittels Verifizierern

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.

Inkrementelle Analyse, Witness Validierung

  • O. Strichman, B. Godlin: Regression Verification – A Practical Way to Verify Programs, VSTTE, LNCS 4171, pp. 496-501, Springer, 2005.
  • M.-C. Jakobs: Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning, SEFM, LNCS 9276, pp. 159-174, Springer, 2015.
  • D. Beyer, S. Löwe, E. Novikov, A. Stahlbauer, P. Wendler: Precision reuse for efficient regression verification, ESEC/FSE, pp. 389-399, ACM, 2013.
  • B. C. Rothenberg, D. Dietsch, M. Heizmann: Incremental Verification Using Trace Abstraction, SAS, LNCS 11002, pp. 364-382, Springer, 2018.
  • T. A. Henzinger, R. Jhala, R. Majumdar, M. A. A. Sanvido: Extreme Model Checking, Verification: Theory and Practice, LNCS 2772, pp. 332-358, Springer, 2003.
  • D. Beyer, M. Dangl, D. Dietsch, M. Heizmann, A. Stahlbauer: Witness validation and stepwise testification across software verifiers, FSE, pp. 721-733, ACM, 2015.
  • D. Beyer, M. Dangl, D. Dietsch, M. Heizmann: Correctness witnesses: Exchanging verification results between verifiers, FSE, pp. 326-337, ACM, 2016.

Testgenerierung, Laufzeitverifikation

  • D. Beyer, A. J. Chlipala, T. A. Henzinger, R. Jhala, R. Majumdar: Generating tests from counterexamples, ICSE, pp. 326-335, IEEE, 2004.
  • D. Beyer, M.-C. Jakob: CoVeriTest: Cooperative Verifier-Based Testing, FASE, LNCS 11424, pp. 389-408, Springer 2019.
  • M. Leucker, C. Schallhart: A brief account of runtime verification, The Journal of Logic and Algebraic Programming, 78 (5), Elsevier, 2009.