News

Midterm 1 inspection; no tutorial this week

Written on 26.05.25 by Anran Wang

Dear Participants,

Midterm 1 can be inspected this Friday (30.05) from 11:30 to 12:30 at E1 3 528.
Please bring your student ID and abide by the rules glued to the door.
Please do not all come at once to avoid long waiting time.

Also, there will be no tutorial this week.

Best,
… Read more

Dear Participants,

Also, there will be no tutorial this week.

Best,
Verification Team

Grace Regulations Concerning Failed Midterm 1

Written on 25.05.25 by Benjamin Kaminski

Hi all,

we will install some grace regulations concerning those of you who did not pass Midterm 1. These are as follows.

If you achieved x₁ < 40 points in Midterm 1:

You may take Midterm 2.
You need to achieve then at least 40 + (40 - x₁) · 2 points in Midterm 2 to be admitted to the… Read more

Hi all,

we will install some grace regulations concerning those of you who did not pass Midterm 1. These are as follows.

If you achieved x₁ < 40 points in Midterm 1:

You may take Midterm 2.
You need to achieve then at least 40 + (40 - x₁) · 2 points in Midterm 2 to be admitted to the final exam.
You cannot claim any bonus points for the final exam.

Those of you who did pass Midterm 1 already are not affected by the above grace regulations at all.

We hope you stay on board!

All the best,

Benjamin

Midterm 1 results

Written on 21.05.25 by Anran Wang

Hi everyone,

We have finished grading the first midterm and uploaded the points. You can find them on your personal status page.

As mentioned previously, the passing threshold was 40 points.
You get 1 bonus point for the final exam for every 10 points gained.

We will announce the date of the… Read more

Hi everyone,

We have finished grading the first midterm and uploaded the points. You can find them on your personal status page.

As mentioned previously, the passing threshold was 40 points.
You get 1 bonus point for the final exam for every 10 points gained.

We will announce the date of the inspection in the coming days.
As a reminder, we will discuss the exam solutions in the next tutorials.

Best,
Verification Team

Midterm important reminders; seating plan; released Sheet 4 sample solution

Written on 16.05.25 by Anran Wang

Dear Students,

Here are some reminders regarding the midterm next Tuesday:
- Time and place: 20.05 14:00 in E2 5 001, a different time and place than the usual lecture.
- Please do not be late!
- Remember to bring your ID/passport and student card.
- Seating plan is available for download in… Read more

Dear Students,

Also, sheet 4 sample solution is available on cms.

Good luck!

Best,
Verification Team

Practise Sheet on LTL and Midterm Office Hour

Written on 13.05.25 by Tobias Gürtler

Dear Students,

The topic of todays lecture, i.e. Linear Time Logic, will be relevant for the midterm exam. In order to help you prepare we have released this week's exercise sheet on LTL early. We also understand that the tutorial which would discuss this sheet only takes place after the midterm,… Read more

Dear Students,

Furthermore, there will not be a lecture next Monday. Instead, we will be offering an Office Hour in the lecture hall where you can stop by and ask any questions you might have.

Finally, we want to highlight again that the midterm exam next week takes place at 14 o'clock in Lecture Hall 1 of E2.5. This means the midterm exam takes place after the usual lecture time slot.

Kind Regards,

The Verification Team

Midterm registration closes on Sunday; released Sheet 3 sample solution and sheet 4

Written on 09.05.25 by Anran Wang

Dear Students,

Here is a reminder that if you wish to take part in the midterm, you should register before midnight of this Sunday (11.05 23:59).

Also, the sheet 3 sample solution and sheet 4 are available on cms.

Have a nice weekend!

Best,

Verification Team

Midterm Registration

Written on 05.05.25 by Tobias Gürtler

Dear Students,

You can now register for the first midterm on your personal status page here in the CMS. If you intend to participate in the first midterm, then you must register until Sunday 11th May at 23:59.

Kind regards,

The Verification Team

Released: Sheet 2 sample solution; sheet 3

Written on 02.05.25 by Anran Wang

Dear Participants,

The sample solution for sheet 2 is released, as well as sheet 3.

Have a nice weekend!

Best,

Verification Team

No tutorial next Thursday; released sheet 2 and sheet 1 sample solution

Written on 25.04.25 by Anran Wang

Dear participants,

Here is a reminder that there will be no tutorial next Thursday, please go to the Friday one instead.

Also, sheet 1 sample solution and sheet 2 are available for download in CMS now.
Note: You can submit an answer to all exercises of sheet 2.

Some hints… Read more

Dear participants,

Here is a reminder that there will be no tutorial next Thursday, please go to the Friday one instead.

Also, sheet 1 sample solution and sheet 2 are available for download in CMS now.
Note: You can submit an answer to all exercises of sheet 2.

Some hints regarding sheet 1:

E1.1: Remember to define the labelling function for all states, otherwise it is not a (complete) function.
E1.3: Giving the top and bottom elements is not enough as a proof for existence of supremum/infimum. You need to prove all subsets have supremum and infimum!

Best,

Verification Team

Released: Sheet 0 sample solution; sheet 1

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

Best,
Verification Team

Midterm 1 time change, date remains

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

Written 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

Best,

Benjamin

Tutorials for this week

Written 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.
However, we offer a replacement tutorial on 17. April, starting from 10:00 c.t. at seminar room E1 3 107 (on the first floor of the same building where the lecture takes place).
If you can not join in this time, we will provide sample solutions to exercise sheet 0, and will be available for questions.

All subsequent Friday tutorials will take place in the regular time and place.

Best,
Verification Team

Show all

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 14:00 – 16:00	Math lecture hall 1 at E2 5
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