Parameterized Verification Swen Jacobs

News

12.07.2022

Sixth Problem Set

Dear students,

I have just uploaded one final problem set, with two exercises.

Even though a couple of lectures were cancelled, we managed to cover the complete contents of the course in the regular lecture time. However, the exercises thus far have not... Read more

Dear students,

I have just uploaded one final problem set, with two exercises.

Even though a couple of lectures were cancelled, we managed to cover the complete contents of the course in the regular lecture time. However, the exercises thus far have not covered the View Abstraction approach, therefore there is this last (small) sheet in the final lecture week.

Please contact Shyam if you want to discuss the exercises this week or next.

04.07.2022

Fifth Problem Set

Dear students,

the fifth exercise sheet is now available under Materials. Submissions (of at least the answers to the short questions) are due next Monday.

The current sheet treats the topics of Lecture 6, there will be one more sheet next week on the topics... Read more

Dear students,

the fifth exercise sheet is now available under Materials. Submissions (of at least the answers to the short questions) are due next Monday.

The current sheet treats the topics of Lecture 6, there will be one more sheet next week on the topics of Lectures 7 and 8.

15.06.2022

Fourth Problem Set

Dear students,

the fourth exercise sheet is now available under Materials. Submissions (of at least the answers to the short questions) are due next Wednesday.

08.06.2022

Change of schedule: Lecture this week

Dear students,

after my medical procedure was postponed again, I decided that we will have a lecture this week (at the regular time), just to avoid more unnecessary delays.

I am very sorry about this change of schedule, but I think and hope that it is better... Read more

Dear students,

after my medical procedure was postponed again, I decided that we will have a lecture this week (at the regular time), just to avoid more unnecessary delays.

I am very sorry about this change of schedule, but I think and hope that it is better than the alternative. If this is a serious problem for you, please let me know.

And by the way, there will not be a new exercise sheet this week, you will get the next one after the upcoming lecture.

31.05.2022

Third Problem Set

Dear students,

the third exercise sheet is now available under Materials. Submissions (of at least the answers to the short questions) are due on Monday.

23.05.2022

Second Problem Set

Dear students,

the second exercise sheet is now available under Materials. Submissions (of at least the answers to the short questions) are due on Friday.

10.05.2022

Scheduling of lectures

Dear students,

I'm sorry to say that this week the lecture again cannot happen. We will meet next week and see what we can do about this. It seems that we are a very small group, which will make re-scheduling easier (but could also be problematic if more people... Read more

Dear students,

I'm sorry to say that this week the lecture again cannot happen. We will meet next week and see what we can do about this. It seems that we are a very small group, which will make re-scheduling easier (but could also be problematic if more people were to drop out).

See you next week!

02.05.2022

First problem set, scheduling of discussion slots and lectures

Dear students,

the first exercise sheet is now available under Materials. Submissions (of at least the answers to the short questions) are due on Friday.

As announced in the first lecture, we will have mandatory (online) discussion slots where you talk about... Read more

Dear students,

the first exercise sheet is now available under Materials. Submissions (of at least the answers to the short questions) are due on Friday.

As announced in the first lecture, we will have mandatory (online) discussion slots where you talk about the exercises with a tutor, and of course also have the option to ask questions about the lecture. To this end, please form groups of 2 (or 3) students, and have at least one of the members of your group submit until Thursday evening (under Submissions -> Discussion Slot Groups) a file that contains the names and matriculation numbers of all members of the group, and the time slots that would fit all of you for the meetings.

Finally, I am sorry to say that there will be more changes to the lecture schedule. My medical procedure that was planned last week had to be postponed to this week, so this week there will again be no lecture. We will discuss how we can make up for the missed lectures, either by having additional meetings, or by covering some of the material in home work.

See you next week!

21.04.2022

Zoom access and start time

Dear students,

we will have our first lecture tomorrow, starting at 10:15 in the CISPA lecture hall.

In case you want to join virtually, please use the following Zoom link:

https://cispa-de.zoom.us/j/91053431273?pwd=Ukg5cnl6UGR2eWw5aWxkTk1aWjNFZz09

This... Read more

Dear students,

we will have our first lecture tomorrow, starting at 10:15 in the CISPA lecture hall.

In case you want to join virtually, please use the following Zoom link:

https://cispa-de.zoom.us/j/91053431273?pwd=Ukg5cnl6UGR2eWw5aWxkTk1aWjNFZz09

This link will be used for all our lectures this semester.

See you tomorrow!

12.04.2022

Time and place of first lecture

Dear students,

since this Friday is a public holiday, our first lecture will be next week, on April 22.

Lectures are planned to be hybrid, i.e., physically at the CISPA lecture hall with the possibility to join via Zoom. I will share details about Zoom access... Read more

Dear students,

since this Friday is a public holiday, our first lecture will be next week, on April 22.

Lectures are planned to be hybrid, i.e., physically at the CISPA lecture hall with the possibility to join via Zoom. I will share details about Zoom access with you before the first lecture.

See you next week!

Show all
 

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

 

Lecture Room: CISPA lecture hall (and online via Zoom)
Lectures: Fridays 10-12
Tutorials: individual discussion slots
Exams: oral exams, July 28/29 (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
Morgan&Claypool, Synthesis Lectures on Distributed Computing Theory (2015)

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



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