News
11.07.2019

ExamDear students, as mentioned in the lecture today, exams will be on July 25 between 10:00 and 18:00. If some time on that day does not work for you, please let me know by email until tomorrow evening. I will send you information on your exact time slot until... Read more Dear students, as mentioned in the lecture today, exams will be on July 25 between 10:00 and 18:00. If some time on that day does not work for you, please let me know by email until tomorrow evening. I will send you information on your exact time slot until next Tuesday, and will still announce in which room the exam will take place. 
10.07.2019

Restrictions at CISPA tomorrowDear students, this is to inform you that tomorrow the water supply in the CISPA building will not work. In particular, bathrooms cannot be used. Please take this into account when you come to the lecture. Sorry for the inconvenience, see you tomorrow! 
28.06.2019

Fifth Problem SetDear Students, since it will be too hot to go outside on the weekend, you might as well spend your time at home with some Parameterized Verification(TM). The fifth and final problem set is now online. As usual, it is due on Thursday before the lecture. Have... Read more Dear Students, since it will be too hot to go outside on the weekend, you might as well spend your time at home with some Parameterized Verification(TM). The fifth and final problem set is now online. As usual, it is due on Thursday before the lecture. Have a nice weekend! 
26.06.2019

Room change tomorrowDear students, due to a special event at CISPA the lecture tomorrow will not be in our usual room, but instead in room 0.07 of the CISPA building (this is the meeting room on the ground floor, straight ahead from the entrance). See you tomorrow! 
13.06.2019

Problem Set 4  SubmissionDear students, you can now submit your solutions for problem set 4. 
07.06.2019

Fourth Problem SetHappy News! The fourth problem set is now available. Please submit solutions until Thursday, 13:59.
Happy News! The fourth problem set is now available. Please submit solutions until Thursday, 13:59.

17.05.2019

Third Problem SetThe new problem set is now available. Please submit solutions until Thursday, 13:59. 
09.05.2019

No Lecture TodayDear Students, due to illness there will be no lecture today. 
03.05.2019

No new Problem Set this weekDear students, as announced during the discussion sessions, there will not be a new Problem Set this week. We have however uploaded a new version of the last one, where the bug in Exercise 1 is fixed. So if you still want to try this (or any other exercise) from... Read more Dear students, as announced during the discussion sessions, there will not be a new Problem Set this week. We have however uploaded a new version of the last one, where the bug in Exercise 1 is fixed. So if you still want to try this (or any other exercise) from the last Problem Set, you can do so. Therefore, discussion sessions next week will be ondemand, i.e., we will expect you only if you submitted something or if you send me an email that you'd like to come and discuss something. But first: have a great weekend! 
30.04.2019

Typo in Second Problem SetPlease note that we uploaded a new version of the problem set 2 where we fixed a typo in exercise 3. 
27.04.2019

Second Problem SetThe new problem set is now available. Please submit solutions until Thursday, 13:59. 
26.04.2019

Rooms for DiscussionsDear students, sorry, we did not communicate the rooms for the discussions. We will have them in our office(s), i.e., in Room 1.13 or 1.16.1 in E1 1. If you couldn't make it to your discussion slot due to the confusion, just drop by sometime between 10:20 and... Read more Dear students, sorry, we did not communicate the rooms for the discussions. We will have them in our office(s), i.e., in Room 1.13 or 1.16.1 in E1 1. If you couldn't make it to your discussion slot due to the confusion, just drop by sometime between 10:20 and 12, or write me a quick email if that is not possible. 
24.04.2019

Discussion SlotsDear students, the CMS seems to have problems with the number of tutorial slots that we have opened  I'm not sure if you can only select from four of them, but in any case we can only see your selection for four of them. So let's do this by hand: can you... Read more Dear students, the CMS seems to have problems with the number of tutorial slots that we have opened  I'm not sure if you can only select from four of them, but in any case we can only see your selection for four of them. So let's do this by hand: can you please include in your submission of the discussion slot groups also two lines Sorry for the inconvenience, see you tomorrow! 
21.04.2019

Discussion slots and first problem setDear students, we hope you have a nice long weekend. Once you get back from it, please use the first submission ("Discussion Slot Groups") to send us a simple txt file with the members of your group for the exercise sheets and discussions, and select (in tutorial... Read more Dear students, we hope you have a nice long weekend. Once you get back from it, please use the first submission ("Discussion Slot Groups") to send us a simple txt file with the members of your group for the exercise sheets and discussions, and select (in tutorial preferences) the possible times for our discussion meeting. It is enough if one member of your group does this. Please do this until Wednesday evening. The first problem set is now also available. It is due before the next lecture, i.e., until Thursday 13:59. 
16.04.2019

TutorialsDear students, the tutorial vote was not successful  for every proposed slot at least one third of the students say they cannot make it, so every choice seems to be very bad. I'll propose a different solution on Thursday. 
12.04.2019

Tutorial vote now openDear students, you should now be able to vote on the time slot for the tutorial. There are three time slots: Mon, Tue, Wed, each from 1012. There are also three possible answers: Preferred, Okay, Not Okay. Please choose "Not Okay" only if it is really not... Read more Dear students, you should now be able to vote on the time slot for the tutorial. There are three time slots: Mon, Tue, Wed, each from 1012. There are also three possible answers: Preferred, Okay, Not Okay. Please choose "Not Okay" only if it is really not possible for you. Please vote until Sunday, then I will announce the decision on Monday. 
11.04.2019

Room changeDear students, since we are a rather small group, we will have the lecture not in the lecture hall 0.05, but in (the more comfortable) room 0.01 of E9 1. See you later! 
Advanced Lecture (Vertiefungsvorlesung), Summer Term 2019, 6 CP
Lecture Room:  E9 1, Room 0.01 
Lectures:  Thursdays, 14:1516:00 
Tutorials:  tba. 
Exams:  tba. 
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 multithreaded 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.
References
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)