News
Discussion SlotsWritten on 26.04.24 by Swen Jacobs Dear students, as announced in the lecture today, please choose the suitable times for a discussion slot, and let us know who is in your group (under Submissions->Discussion Slot Groups) until Monday evening. It is enough if one person per group does this. If the available times don't work for you,… Read more Dear students, as announced in the lecture today, please choose the suitable times for a discussion slot, and let us know who is in your group (under Submissions->Discussion Slot Groups) until Monday evening. It is enough if one person per group does this. If the available times don't work for you, please let us know. We will let you know on Tuesday which slot has been assigned to you. |
First Lecture: Room changeWritten on 18.04.24 by Swen Jacobs Dear students, please note that our first lecture (tomorrow at 10:15) will take place in the CISPA lecture hall (C0, room 0.05), and not in our usual room 0.02. |
Advanced Lecture (Vertiefungsvorlesung), Summer Term 2024, 6 CP
| Lecture Room: | CISPA: room 0.02 |
| Lectures: | Fridays 10-12 |
| Tutorials: | individual discussion slots |
| Exams: | oral exams, August 01/02 (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)