News
Released: Sheet 0 sample solution; sheet 1Written on 17.04.25 by Anran Wang Dear participants, Sheet 0 sample solution and sheet 1 are available for download in CMS now. Happy easter!
|
Midterm 1 time change, date remainsWritten on 15.04.25 (last change on 15.04.25) by Anran Wang Dear participants of Verification, Due to the large number of registrations on CMS and the limited capacity of HS003, we have to move midterm 1 to 14-16 o’clock (still on 20.05) to Math lecture hall 1 at E2 5.
Best, Verification team |
Blackboard PhotosWritten on 15.04.25 by Benjamin Kaminski We have now uploaded Photos of the blackboard drawings and writings (thanks to Lucas for taking them). Please beware that this is a best effort service. It is and will be neither complete nor comprehensive as stand-alone material. But we do hope it complements the course material and is useful to… Read more We have now uploaded Photos of the blackboard drawings and writings (thanks to Lucas for taking them). Please beware that this is a best effort service. It is and will be neither complete nor comprehensive as stand-alone material. But we do hope it complements the course material and is useful to you.
Best, Benjamin |
Tutorials for this weekWritten on 14.04.25 (last change on 14.04.25) by Anran Wang Dear participants, The tutorials have been assigned. If you have any problem, please contact us through discord or via email. Alternative tutorial replacing the first Friday tutorial (This does not concern participants of the Thursday tutorial.) Due to public holiday (Karfreitag) on 18.… Read more Dear participants, The tutorials have been assigned. If you have any problem, please contact us through discord or via email. Alternative tutorial replacing the first Friday tutorial (This does not concern participants of the Thursday tutorial.) Due to public holiday (Karfreitag) on 18. April, there will be no tutorial on that Friday. All subsequent Friday tutorials will take place in the regular time and place.
|
Verification
SS 2025
Lecturer | Prof. Benjamin Kaminski |
TA | Tobias Gürtler, Lucas Kehrer, Anran Wang |
Introduction
Compute systems are everywhere, including in critical scenarios where human lives are at stake (airplanes, hospitals, nuclear power plants, etc.). It is paramount that such systems are safe. But what does "safe" even mean?
In this lecture, we will explore various logics for specifying and techniques for proving with mathematical rigor that systems are safe. Time permitting, we will also peek into methods for reasoning about quantitative properties of probabilistic systems.
Topics which we will cover include:
- Model checking
- Linear temporal logic (LTL)
- Computation tree logic (CTL)
- Hoare logic
- Weakest preconditions / predicate transformers
- k-induction
- Probabilistic verification
Structure
This course consists of two weekly lectures and one tutorial. The lectures take place Mondays from 10:00 m.c.t. – 12:00, and Tuesdays from 12:00 c.t. – 14:00 (see below) at E1 3, Lecture Hall III (0.03.1) starting from 8. April.
For the tutorial, we offer two dates: Either Thursdays or Fridays 10:00 – 12:00 in seminar room SR 014 (Thursdays) or SR 015 (Fridays) both in building E1 3 starting from 17th April.
There will be two midterm exams taking place during the lecture dates. Passing the midterms is required to be admitted to the final exam. Details announced in the first lecture. Homework is not required to be admitted to the exam.
There will be weekly homework, which consists two parts: Part 1 (basic) and Part 2 (advanced). Homework submission is voluntary. Upon submission, Part 1 will be corrected and returned to you. Sample solutions will be provided for Part 2. In the tutorial, we will discuss last week's homework and answer questions.
Check the timetable for time and place of lectures, tutorials, midterms, and final exams.
Requirements
Very Strongly Recommended | Programmierung 1 Programmierung 2 Grundzüge der Theoretischen Informatik |
Recommended | Concurrent Programming |
Timeline / Deadlines (Tentative)
Also available in the timetable.
Lecture | Mo. 10:00 m.c.t – 12:00 Tu. 12:00 c.t. – 14:00 |
E1 3, Lecture Hall III (0.03.1) |
Tutorial | Th. 10:00 c.t. – 12:00 Fr. 10:00 c.t. – 12:00 |
E1 3, Seminar Room 014 (Thursdays) E1 3, Seminar Room 015 (Fridays) |
Midterm 1 | 20.5.2025 12:00 – 14:00 | E1 3, Lecture Hall III (0.03.1) |
Midterm 2 | 24.6.2025 12:00 – 14:00 | E1 3, Lecture Hall III (0.03.1) |
Exam | 19.08.2025 14:30-16:30 | E2 5, Lecture Hall I (001.0) |
Retake | 16.09.2025 14:30-16:30 | E1 3, Lecture Hall II (0.02.1) |
w/c = week commencing |
See also the course website. The website on CMS is, however, more up-to-date.
Textbook
- Baier, Christel, and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press Ser. Cambridge, Massachusetts London, England: The MIT Press, 2008.
- Benjamin Lucien Kaminski. Advanced Weakest Precondition Calculi for Probabilistic Programs. 2019