Parameterized Verification Swen Jacobs

Registration for this course is open until Friday, 12.04.2019 23:59.


Currently, no news are available

Advanced Lecture (Vertiefungsvorlesung), Summer Term 2019, 6 CP

Lecture Room: E9 1, Room 0.05
Lectures: Thursdays, 14:15-16:00
Tutorials: tba.
Exams: tba.


We consider the problem of providing correctness and security guarantees for systems that scale with some parameter, e.g., the number of nodes in a network, the number of concurrent processes in a multi-threaded program, or the size of a data structure that a program operates on. Most systems are expected to scale in one or several parameters, but correctness and security guarantees are usually only given for fixed parameter values. In contrast, parameterized verification is the problem of obtaining correctness guarantees for all parameter values. In this course, we will look at methods for parameterized verification and investigate their capabilities and limitations.

The course is aimed at students interested in the theoretical concepts behind parameterized verification, which generalize system models, specification formalisms and proof methods from standard verification approaches. The course picks up on some of the topics of the core lecture "Verification", which is however not a prerequisite for this course.


The course will be based on the following textbook, supplemented by other sources as necessary:

Decidability of Parameterized Verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder
Morgan&Claypool, Synthesis Lectures on Distributed Computing Theory (2015)

(hardcopies should be available in the library when the semester starts, a PDF will be made available through CMS)

Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators