Parameterized Verification Swen Jacobs

News

11.07.2019

Exam

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... 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 tomorrow

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!

28.06.2019

Fifth Problem Set

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... 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 tomorrow

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!
 

13.06.2019

Problem Set 4 - Submission

Dear students,

you can now submit your solutions for problem set 4.

07.06.2019

Fourth Problem Set

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


The slides for Lecture 7 have also been updated, such that the steps of the proof on Slides 31ff are now visible in the pdf (which is useful in general, and in... Read more

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


The slides for Lecture 7 have also been updated, such that the steps of the proof on Slides 31ff are now visible in the pdf (which is useful in general, and in particular for the problem set).

17.05.2019

Third Problem Set

The new problem set is now available. Please submit solutions until Thursday, 13:59.

09.05.2019

No Lecture Today

Dear Students,

due to illness there will be no lecture today.

03.05.2019

No new Problem Set this week

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... 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 on-demand, 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 Set

Please 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 Set

The new problem set is now available. Please submit solutions until Thursday, 13:59.

26.04.2019

Rooms for Discussions

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... 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 Slots

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... 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
Preferred: ...
Okay: ...
with the times that you are available?
The possible time slots are Fridays and Mondays from 9 to 11, every 20 minutes.

Sorry for the inconvenience, see you tomorrow!

21.04.2019

Discussion slots and first problem set

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... 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

Tutorials

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.

12.04.2019

Tutorial vote now open

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 10-12. 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 10-12. 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 change

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!

Show all
 

Advanced Lecture (Vertiefungsvorlesung), Summer Term 2019, 6 CP

Lecture Room: E9 1, Room 0.01
Lectures: Thursdays, 14:15-16: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 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 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)



Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators