Course: Advanced Verification of Software and Systems

Course: Advanced Verification of Software and Systems

Schedule:

• Lecture (Prof. Dr. Stefan Leue)
  Monday  13:13 - 15:00             Start: 12 April 2021
  Thursday  10:00 - 11:30         

• Tutorial (Fabian Marquart)
  Wednesday 15:15 - 16:45        Start: 14 April 2021

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.

Course content

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

Online course. Pre-recorded lectures. Q&A-Sessions at regular intervals.

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 assessment

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 9

Weekly teaching hours

 SWS 4  (+ tutorial 2)