Organizers	Prof. Benjamin Kaminski, Tobias Gürtler, Anran Wang
Places	E1 3, Lecture Hall III (0.03.1)

---

InTroduction

Have you wondered whether your programs are safe? What does “safe” even mean? If so, this lecture is for you.

In this lecture, we will explore various model checking techniques, from system modelling, property specification, to the use of linear temporal logic (LTL) and computation tree logic (CTL). Additionally, we will apply these methods to reason about probabilistic programs. Beyond model checking, we will also cover other verification methods, such as Hoare logic, predicate transformers, and more.

Topics which we will cover include:

• Modeling concurrent systems
• Linear temporal logic
• Computation tree logic
• Probabilistic programming (a currently trending modeling paradigm in machine learning)
• Hoare logic
• Dijkstra’s predicate transformers
• and many more…

structure

This course consists of two weekly lectures and 1-3 tutorials. The lectures take place Mondays from 10 to 12, and Tuesdays from 12 to 14 (see below) at E1 3, Lecture Hall III (0.03.1). The tutorials’ time and place are to be determined.

There will (likely) be a midterm, passing the midterm is required to gain entry to the final exam. There will be no graded weekly homework, but we organize weekly tutorials to help internalize the lecture material and prepare for the final exam.

Requirements (Tentative)

Mandatory	Programmierung 1 Programmierung 2 Grundzüge der Theoretischen Informatik
Recommended	Introduction to Computational Logic Automata, Games and Verification
Ideal

Timeline / Deadlines (tentative)

Lecture	Mo. 10 – 12 Tu. 12 – 14	E1 3, Lecture Hall III (0.03.1)
Tutorial	TBD

Textbook

• Baier, Christel, and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press Ser. Cambridge, Massachusetts London, England: The MIT Press, 2008.
• …