Main Page

News

Re-Exam

Written on 04.09.19 by Swen Jacobs

Dear students,

we will offer a re-exam in the last week of September. It will be an oral exam, just like the last one.

If you want to take the re-exam, please let me know if the morning of September 25 suits you, or propose a different time in the same week.

Exam Results and Re-exam

Written 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 re-exam, we can arrange a time in the week 23-27 September. In this case, please let me know until 15 September.

Exam Time and Place

Written 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,

All exams on Thursday will take place in Room 1.10.2 in E1 1 (next to my office).

Exam times, no lecture this week

Written 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!

Exam

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

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

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

Written 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 - Submission

Written on 13.06.19 by Mouhammad Sakr

Dear students,

you can now submit your solutions for problem set 4.

Fourth Problem Set

Written on 07.06.19 by Swen Jacobs

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

Third Problem Set

Written on 17.05.19 by Swen Jacobs

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

No Lecture Today

Written on 09.05.19 by Swen Jacobs

Dear Students,

due to illness there will be no lecture today.

No new Problem Set this week

Written 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,

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!

Typo in Second Problem Set

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

Written on 27.04.19 by Swen Jacobs

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

Rooms for Discussions

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

Written 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,

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!

Discussion slots and first problem set

Written 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,

The first problem set is now also available. It is due before the next lecture, i.e., until Thursday 13:59.

Tutorials

Written 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 open

Written 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 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… Read more

Dear students,

Please vote until Sunday, then I will announce the decision on Monday.

Room change

Written 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!

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)