Main Page

News

Re-exam: date confirmed, registration possible

Written on 26.08.24 by Swen Jacobs

Dear students,

the time and date for the re-exam has been confirmed as

Friday, Sep 27, 9-13h

you should be able to register now. As usual, registration and un-registration will be possible until one week before the exam.

Exam grades, Re-exam

Written on 09.08.24 by Swen Jacobs

Dear students,

your exam grades should now be available in LSF.

The re-exam is planned for September 27, between 9 and 13h, but the date is not officially confirmed yet. As I will be on vacation for the next 2 weeks, I will only be able to confirm it after that.

Exam on Friday

Written on 30.07.24 by Swen Jacobs

Dear students,

everybody who has registered for the exam should now be able to see their assigned time slot in the CMS profile under "Exam Slot". Each slot is 30 min, the exam itself is 15-20 min. Please be there 5 minutes before your slot begins so that we don't have any delays.

The exam will… Read more

Dear students,

The exam will take place in room 3.21 in the CISPA building.

Location of lecture tomorrow

Written on 18.07.24 by Swen Jacobs

Dear students,

as announced in the last lecture, tomorrow's lecture (and the discussion group that would usually be in the same room as the lecture) will be held

in lecture hall 1 of the computer science building E1 3.

See you tomorrow!

Eighth Exercise Sheet

Written on 12.07.24 by Tom Baumeister

Dear students,

the 8th exercise sheet is now available. Please hand in solutions until Thursday evening.

Open Submission Slot for Sheet 7

Written on 11.07.24 by Tom Baumeister

Dear students,

You can now upload your submissions for the current exercise sheet until 23:59.

Seventh Exercise Sheet

Written on 05.07.24 by Tom Baumeister

Dear students,

the 7th exercise sheet is now available. Please hand in solutions until Thursday evening.

Sixth Exercise Sheet

Written on 28.06.24 by Paul Eichler

Dear students,

the sixth exercise sheet is now available under Materials. Please hand in solutions until Thursday evening.

No exercise sheet & no tutorials next week

Written on 21.06.24 by Paul Eichler

Dear students,
As mentioned in today's lecture, we won't have an exercise sheet for this week's lecture. Consequently, we won't have tutorial sessions next week, only a lecture.

Lecture tomorrow canceled

Written on 13.06.24 by Swen Jacobs

Dear students,

due to ongoing health issues we again have to cancel tomorrow's lecture. For your convenience, we will also postpone the discussion of the current exercise sheet to next week.

Lecture tomorrow canceled

Written on 06.06.24 by Swen Jacobs

Dear students,

due to health issues I have to cancel tomorrow's lecture. For your convenience, we will also postpone the discussion of the current exercise sheet to next week.

Fifth Exercise Sheet

Written on 27.05.24 by Swen Jacobs

Dear students,

the 5th exercise sheet is now available. As there will be no lecture and no tutorials this week, you only have to submit the solutions by Thursday next week.

I have also updated the slides of Lecture 6 (fixed new MESI example and some typos).

Fourth Exercise Sheet

Written on 17.05.24 by Tom Baumeister

Dear students,

the fourth exercise sheet is now available under Materials. Please hand in solutions until Thursday evening.

Lecture Slides, Exercise Sheet

Written on 13.05.24 by Swen Jacobs

Dear students,

I have now uploaded a fixed version of the slides for Lecture 4, fixing a few typos.

Regarding the exercise sheet, note in particular that in the MESI example, the initial state is not (\infty,0,0,0), but (0,0,0,\infty) - as the local states are in this case ordered (M,E,S,I), and… Read more

Dear students,

I have now uploaded a fixed version of the slides for Lecture 4, fixing a few typos.

Third exercise sheet

Written on 10.05.24 by Shyam lal Karra

Dear students,

The third exercise sheet is now available under Materials. Please hand in solutions until Thursday evening.

Lecture today: room, slides

Written on 10.05.24 by Swen Jacobs

Dear students,

as a reminder, the lecture today will be held in the CISPA lecture hall again. I have also just uploaded preliminary slides for today's lecture.

Second Exercise Sheet

Written on 03.05.24 by Swen Jacobs

Dear students,

the second exercise sheet is now available under Materials. Please hand in solutions until Thursday evening.

Discussion Slots Assigned

Written on 30.04.24 by Swen Jacobs

Dear students,

the discussion slots have now been assigned, you should be able to see them. Tutorials start this Friday.

Due to some difficulties with the CMS, we are not perfectly sure that everybody has been assigned a slot that fits their preferences. If your current slot does not work at all… Read more

Dear students,

the discussion slots have now been assigned, you should be able to see them. Tutorials start this Friday.

Due to some difficulties with the CMS, we are not perfectly sure that everybody has been assigned a slot that fits their preferences. If your current slot does not work at all for you, please let us know and we will try to solve the problem.

In case you have received an email before with a different assignment than is now visible: the current assignment counts.

First Exercise Sheet

Written on 29.04.24 by Swen Jacobs

Dear students,

the first exercise sheet is now available under Materials. Please hand in solutions before the first discussion slots, i.e., until Thursday evening.

Discussion Slots

Written on 26.04.24 by Swen Jacobs

Dear students,

as announced in the lecture today, please choose the suitable times for a discussion slot, and let us know who is in your group (under Submissions->Discussion Slot Groups) until Monday evening. It is enough if one person per group does this. If the available times don't work for you,… Read more

Dear students,

We will let you know on Tuesday which slot has been assigned to you.

First Lecture: Room change

Written on 18.04.24 by Swen Jacobs

Dear students, please note that our first lecture (tomorrow at 10:15) will take place in the CISPA lecture hall (C0, room 0.05), and not in our usual room 0.02.

Show all

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

Lecture Room:	CISPA: room 0.02
Lectures:	Fridays 10-12
Tutorials:	individual discussion slots
Exams:	oral exams, August 01/02 (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
Springer, Synthesis Lectures on Distributed Computing Theory (2015)

(hardcopies should be available in the library, a PDF is available through CMS)