News
ReExamWritten on 04.09.19 by Swen Jacobs Dear students, we will offer a reexam in the last week of September. It will be an oral exam, just like the last one. If you want to take the reexam, please let me know if the morning of September 25 suits you, or propose a different time in the same week. 
Exam Results and ReexamWritten on 30.07.19 by Swen Jacobs Dear Students, the exam results are now visible here and in the LSF. If you want to take the reexam, we can arrange a time in the week 2327 September. In this case, please let me know until 15 September. 
Exam Time and PlaceWritten on 23.07.19 by Swen Jacobs Dear Students, in light of the weather forecast for Thursday we make the following offer to all students that are currently scheduled to have their exam at 14:00 or later: if you want, we can reschedule your exam to a time between 8:00 and 10:00 in the morning. Please let me know if you would… Read more Dear Students, in light of the weather forecast for Thursday we make the following offer to all students that are currently scheduled to have their exam at 14:00 or later: if you want, we can reschedule your exam to a time between 8:00 and 10:00 in the morning. Please let me know if you would prefer that. All exams on Thursday will take place in Room 1.10.2 in E1 1 (next to my office). 
Exam times, no lecture this weekWritten on 17.07.19 by Swen Jacobs Dear students, you should now all have received an email with your personal exam time. If not, please let me know ASAP. The room for the exam will be announced next week. Also, remember that, as announced last week, tomorrow there will be no lecture. All the best for your exam preparation! 
ExamWritten on 11.07.19 by Swen Jacobs 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… 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. 
Restrictions at CISPA tomorrowWritten on 10.07.19 by Swen Jacobs Dear 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! 
Fifth Problem SetWritten on 28.06.19 by Swen Jacobs 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! 
Room change tomorrowWritten on 26.06.19 by Swen Jacobs Dear 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! 
Problem Set 4  SubmissionWritten on 13.06.19 by Mouhammad Sakr Dear students, you can now submit your solutions for problem set 4. 
Fourth Problem SetWritten on 07.06.19 by Swen Jacobs Happy News! The fourth problem set is now available. Please submit solutions until Thursday, 13:59.

Third Problem SetWritten on 17.05.19 by Swen Jacobs The new problem set is now available. Please submit solutions until Thursday, 13:59. 
No Lecture TodayWritten on 09.05.19 by Swen Jacobs Dear Students, due to illness there will be no lecture today. 
No new Problem Set this weekWritten on 03.05.19 by Swen Jacobs 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… 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! 
Typo in Second Problem SetWritten on 30.04.19 by Mouhammad Sakr Please note that we uploaded a new version of the problem set 2 where we fixed a typo in exercise 3. 
Second Problem SetWritten on 27.04.19 by Swen Jacobs The new problem set is now available. Please submit solutions until Thursday, 13:59. 
Rooms for DiscussionsWritten on 26.04.19 by Swen Jacobs 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… 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. 
Discussion SlotsWritten on 24.04.19 by Swen Jacobs 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… 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! 
Discussion slots and first problem setWritten on 21.04.19 by Swen Jacobs 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… 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. 
TutorialsWritten on 16.04.19 by Swen Jacobs Dear 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. 
Tutorial vote now openWritten on 12.04.19 by Swen Jacobs 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… 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. 
Room changeWritten on 11.04.19 by Swen Jacobs Dear 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)