News
First Exercise SheetWritten on 17.04.26 by Tom Baumeister Dear students, the first exercise sheet is now available under Information -> Materials. Please hand in your solution until 23.04.2026 23:59. |
Submission of Discussion Slot Groups and TimesWritten on 15.04.26 by Swen Jacobs Dear students, we hope you have formed groups for the discussion slots/tutorials by now. To distribute the time slots, please submit until Friday (under Submissions -> Discussion Slot Groups) a txt or pdf file with the following: 1. the full names of the (2 or 3) group members 2. the time… Read more Dear students, we hope you have formed groups for the discussion slots/tutorials by now. To distribute the time slots, please submit until Friday (under Submissions -> Discussion Slot Groups) a txt or pdf file with the following: 1. the full names of the (2 or 3) group members 2. the time slots out of the following list that would suit your group: Friday 9-10, Friday 12-13, Friday 13-14, Friday 14-15 If none of these work for you, please let us know and we will figure something out. We will then assign the discussion slots and they will start on April 24. |
Change of Lecture RoomWritten on 10.04.26 by Swen Jacobs Dear students, since the number of registrations is higher than expected, the lecture will be held in the lecture hall of CISPA (room 0.05), and not in the room originally announced. See you later! |
Advanced Lecture (Vertiefungsvorlesung), Summer Term 2026, 6 CP
| Lecture Room: | CISPA: lecture hall (room 0.05) |
| Lectures: | Fridays 10-12 |
| Tutorials: | individual discussion slots |
| Exams: | oral exams, July 16/17 (tentative) |
Topic
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 highly recommended, but not a prerequisite for this course.
References
The course will be loosely based on the following textbook, supplemented by recent research results in the area:
Decidability of Parameterized Verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder
Springer, Synthesis Lectures on Distributed Computing Theory (2015)
(hardcopies should be available in the library, a PDF is available through CMS)