Automatic Software Verification

Automatic Software Verification (ASV)

Lecturer: Prof. Dr. Marie-Christine Jakobs

Typically, the course is offered each summer term.

Current Course Information

In summer term 2021, the course is offered online. You are mainly supposed to self-study the course content. However, you are encouraged to participate in the weekly question and answering session to get in touch and discuss the weekly topic with the teacher and other students. In addition, there will be several asynchronous offers to get feedback or ask questions.

Di 12:00-13::00, Question & Answering session via Zoom

Course Content

The course deals with approaches for automatic software verification. Topics of the course are:

  • operational semantics of sequential programs
  • configurable program analysis (including configuration of dataflow analyses and model checking)
  • bounded model checking
  • k-induction
  • cooperative verification, especially conditional model checking

After successful participation, students can name a number of techniques for automatic software verification. They can describe and classify the techniques and formally define their foundations. Furthermore, students can apply the techniques to examples and are able to develop new configurable program analyses.

Recommended Previous Knowledge

Knowledge of the first four semesters of the Bachelor's degree, especially propositional and predicate logic

Literature

Semantics

  • 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.

Domains, Program Analysis, 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-Induction

  • 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.