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)