Course: Advanced verification of software and systems

Schedule:

  • Course (Prof. Dr. Stefan Leue)
    Tuesday   13:30 - 15:00      Room PZ 901          Start: 22 October 2024
    Thursday  10:00 - 11:30      Room PZ 901          Start: 24 October 2024
  • Tutorial (David Boetius)
    Monday 13:30 - 15:00         Room PZ 901          Start: 28 October 2024

 

Description:

Workload

270 hours, of which 84 hours are spent in class and 186 hours of self study

Prerequisites

While this course builds to some extent on material covered in the precursory course "Verification of Software and Systems" it will be possible to attend this course without having attended this precursory course. Relevant content from the precursory course will be repeated in this course. In addition, a complete recording of the precursory course is available. Bachelor-level familiarity with the foundations of the theory of computing, discrete mathematics, logic, language theory and stochastics are expected.

Contents

This newly designed course will cover some advanced topics in the Verification of Software and Systems, with a special focus on formal verification techniques . After a brief review of the techniques around LTL and CTL model checking, combating the combinatorial state space explosion problem will be addressed. Here, the course will, in particular, look at partial order reduction and abstraction techniques. In order to enable the verification of a wider range of system types, the course will introduce into the model checking-based verification of real-time and probabilistic systems. Further, the dircect analysis of code, referred to as software model checking, will be presented. Finally, recent research results and directions will be discussed. A number of practical software verification tools will be presented and used during the tutorials.

Teaching methods

Please register in ZEuS, which will register you automatically in ILIAS. We will distribute all information regarding course organization as well as all course materials via ILIAS.

Learning objectives

It is the objective of this course to enable students to assess and use the software and system verification technologies, in particular model checking, that will be presented in this course. The participants of this course will be enabled to use model checking technologies in practical problems and to estimate and anticipate the possibilities as well as the limitations of using this technology in practical software and systems engineering projects. The will also be enabled to chose adequate tool support for the solution of practical model checking problems.

Course literature

C. Baier and J.-P. Katoen, Principles of Model Checking, MIT Press, 2008
E. Clarke, O. Grumberg, D. Kroening, D. Peled and H. Veith, Model Checking, second edition, MIT Press, 2018
E. Clarke, T. Henzinger, H. Veith and R. Bloem, (Eds.), Handbook of Model Checking, Springer, 2018

Record of academic assessments

Oral or written examination at the end of the semester
Active participation in the excercises

Remark

The course will be taught in English. All course materials will be in English.

Credits

ECTS-points: 9

Weekly teaching hours

SWS: 4 (+ Tutorial: 2)