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

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.

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 will be announced later). Homework is not required to be admitted to the exam.

There will be weekly homework, which consists two parts: Part 1 (recommended) 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. 

 

Requirements

Very Strongly Recommended	Programmierung 1   Programmierung 2  Grundzüge der Theoretischen Informatik
Recommended	Concurrent Programming

 

 

Timeline / Deadlines (Tentative)

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 – 12:00  Fr. 10:00 – 12:00	E1 3, Seminar Room 014 (Thursdays) E1 3, Seminar Room 015 (Fridays)
Midterm 1	likely w/c 19.5.2025	E1 3, Lecture Hall III (0.03.1)
Midterm 2	likely w/c 23.6.2025	E1 3, Lecture Hall III (0.03.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