News
Sixth Problem SetWritten on 12.07.22 by Swen Jacobs Dear students, I have just uploaded one final problem set, with two exercises. Even though a couple of lectures were cancelled, we managed to cover the complete contents of the course in the regular lecture time. However, the exercises thus far have not covered the View Abstraction approach,… Read more Dear students, I have just uploaded one final problem set, with two exercises. Even though a couple of lectures were cancelled, we managed to cover the complete contents of the course in the regular lecture time. However, the exercises thus far have not covered the View Abstraction approach, therefore there is this last (small) sheet in the final lecture week. Please contact Shyam if you want to discuss the exercises this week or next. |
Fifth Problem SetWritten on 04.07.22 by Swen Jacobs Dear students, the fifth exercise sheet is now available under Materials. Submissions (of at least the answers to the short questions) are due next Monday. The current sheet treats the topics of Lecture 6, there will be one more sheet next week on the topics of Lectures 7 and 8. |
Fourth Problem SetWritten on 15.06.22 by Swen Jacobs Dear students, the fourth exercise sheet is now available under Materials. Submissions (of at least the answers to the short questions) are due next Wednesday. |
Change of schedule: Lecture this weekWritten on 08.06.22 by Swen Jacobs Dear students, after my medical procedure was postponed again, I decided that we will have a lecture this week (at the regular time), just to avoid more unnecessary delays. I am very sorry about this change of schedule, but I think and hope that it is better than the alternative. If this is a… Read more Dear students, after my medical procedure was postponed again, I decided that we will have a lecture this week (at the regular time), just to avoid more unnecessary delays. I am very sorry about this change of schedule, but I think and hope that it is better than the alternative. If this is a serious problem for you, please let me know. And by the way, there will not be a new exercise sheet this week, you will get the next one after the upcoming lecture. |
Third Problem SetWritten on 31.05.22 by Swen Jacobs Dear students, the third exercise sheet is now available under Materials. Submissions (of at least the answers to the short questions) are due on Monday. |
Second Problem SetWritten on 23.05.22 by Swen Jacobs Dear students, the second exercise sheet is now available under Materials. Submissions (of at least the answers to the short questions) are due on Friday. |
Scheduling of lecturesWritten on 10.05.22 by Swen Jacobs Dear students, I'm sorry to say that this week the lecture again cannot happen. We will meet next week and see what we can do about this. It seems that we are a very small group, which will make re-scheduling easier (but could also be problematic if more people were to drop out). See you next week! |
First problem set, scheduling of discussion slots and lecturesWritten on 02.05.22 by Swen Jacobs Dear students, the first exercise sheet is now available under Materials. Submissions (of at least the answers to the short questions) are due on Friday. As announced in the first lecture, we will have mandatory (online) discussion slots where you talk about the exercises with a tutor, and of… Read more Dear students, the first exercise sheet is now available under Materials. Submissions (of at least the answers to the short questions) are due on Friday. As announced in the first lecture, we will have mandatory (online) discussion slots where you talk about the exercises with a tutor, and of course also have the option to ask questions about the lecture. To this end, please form groups of 2 (or 3) students, and have at least one of the members of your group submit until Thursday evening (under Submissions -> Discussion Slot Groups) a file that contains the names and matriculation numbers of all members of the group, and the time slots that would fit all of you for the meetings. Finally, I am sorry to say that there will be more changes to the lecture schedule. My medical procedure that was planned last week had to be postponed to this week, so this week there will again be no lecture. We will discuss how we can make up for the missed lectures, either by having additional meetings, or by covering some of the material in home work. See you next week! |
Zoom access and start timeWritten on 21.04.22 by Swen Jacobs Dear students, we will have our first lecture tomorrow, starting at 10:15 in the CISPA lecture hall. In case you want to join virtually, please use the following Zoom link: https://cispa-de.zoom.us/j/91053431273?pwd=Ukg5cnl6UGR2eWw5aWxkTk1aWjNFZz09 This link will be used for all our… Read more Dear students, we will have our first lecture tomorrow, starting at 10:15 in the CISPA lecture hall. In case you want to join virtually, please use the following Zoom link: https://cispa-de.zoom.us/j/91053431273?pwd=Ukg5cnl6UGR2eWw5aWxkTk1aWjNFZz09 This link will be used for all our lectures this semester. See you tomorrow! |
Time and place of first lectureWritten on 12.04.22 by Swen Jacobs Dear students, since this Friday is a public holiday, our first lecture will be next week, on April 22. Lectures are planned to be hybrid, i.e., physically at the CISPA lecture hall with the possibility to join via Zoom. I will share details about Zoom access with you before the first… Read more Dear students, since this Friday is a public holiday, our first lecture will be next week, on April 22. Lectures are planned to be hybrid, i.e., physically at the CISPA lecture hall with the possibility to join via Zoom. I will share details about Zoom access with you before the first lecture. See you next week! |
Advanced Lecture (Vertiefungsvorlesung), Summer Term 2022, 6 CP
| Lecture Room: | CISPA lecture hall (and online via Zoom) |
| Lectures: | Fridays 10-12 |
| Tutorials: | individual discussion slots |
| Exams: | oral exams, July 28/29 (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
Morgan&Claypool, Synthesis Lectures on Distributed Computing Theory (2015)
(hardcopies should be available in the library, a PDF is available through CMS)