Automatic Software Verification (ASV)

This integrated course looks into several techniques for automatic software verification. More details on the covered topics can be found under the section course content.

Automatic Software Verification (ASV)

Lecturer: Prof. Dr. Marie-Christine Jakobs

The course is no longer offered. The course was offered the last time in summer term 2022.

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)
  • counterexample-guided abstraction refinement (CEGAR)
  • 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.