Model Checking (SS 2025)
Table of Content
Content
Model checking is a widely used technique for automatic verification and debugging of both software and hardware, with the power to reveal subtle errors that remain undiscovered using testing. Therefore, model checking is an effective technique to expose potential design errors and improve software and hardware reliability, and it is gaining wide industrial acceptance. Its inventors Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis have been awarded the significant Turing award in 2007. How does model checking work? What are its underlying principles? This is the focus of this course! Model checking is based on well-known paradigms from automata theory, graph algorithms, logic, and data structures. In the course, we first explain what these models actually are. We introduce temporal logics (e.g., LTL and CTL) to formalize various classes of system properties such as safety, liveness and fairness, and discuss in detail model checking algorithms for these logics.Practicals
As part of the practicals accompanying the lecture, you will build your own simple model checker that supports two popular algorithms. Here, we first introduce you to the basics of hardware implementations, safety and liveness, as well as symbolic representation and SMT solvers. Afterward, we use these building blocks to implement the bounded model checking algorithm you will learn in the lecture. Finally, we extend the BMC implementation so it can make unbounded proofs using K-Induction.Material
The course is based on:Model Checking, second edition by Edmund M. Clarke Jr., Orna Grumberg, Daniel Kröning, Doron Peled, Helmut Veith MIT Press, ISBN-13: 978-0262038836 ISBN-10: 0262038838
Model Checking.
The lectures on probabilistic Model Checking are based on
Principles of Model Checking by Christel Baier and Joost-Pieter Katoen MIT Press, ISBN-13: 978-0262026499 ISBN-10: 026202649X
Principles of Model Checking.
Previous years: SS2021 SS2022 SS2023 SS2024
Administrative Information
Lecture
There are two ways to get a grade for the lecture: Option 1: You participate in class and do the homework. Option 2: You take an exam. If you partisipate in class and you do the homework, you will get a grade for the course. To get a passing grade, you can miss at most two classes and skip at most two homework exercises. You get a 0-100 mark as the average of all homework exercises. Non-handed exercises count as 0 points for the average. From the 0-100 mark, the final grades are distributed as follows:| Points | Grade |
| < 50 | 5 |
| 50 - 62.4 | 4 |
| 62.5 - 74.9 | 3 |
| 75 - 87.4 | 2 |
| 87.5 - 100 | 1 |
Practicals
The practicals are done individually and consist of three assignments with point distribution 30/40/30. We follow the standard grading scheme, where you need more than 50% of the points for passing, and all other grades are distributed evenly in 12.5% increments. In addition to automated tests, we also rely on manual inspection of your submissions. The assignments will usually be presented after the lecture. The practicals time slots will be used for assignment presentations, tutorials and question hours. Feel free to ask questions anytime in the Discord channel as well. Also, take advantage of our new and feature-rich test system and see how well your submissions are doing against our test suite and other students.Lecture Schedule
| Date | Type | Topic | Lecturer | Slides | Homework |
|---|---|---|---|---|---|
| 04. 03. 2025 | Lecture | Intro | Roderick | mc01-intro mc03-modeling | hw1 |
| 11. 03. 2025 | Lecture | SAT-Based Model Checking (BMC, k-induction) - Chapter 10 | Roderick | mc10-sat-1-bmc | hw2 |
| 18. 03. 2025 | Lecture | SAT-Based Model Checking (Interpolation) - Chapter 10 | Roderick | mc10-sat-2-kinduction mc10-sat-3-interpolation | hw3 pdf hw3 zipped tex |
| 25. 03. 2025 | Lecture | SAT-Based Model Checking (PDR) - Chapter 10 | Roderick | hw4 mc10-sat-4-pdr | |
| 01. 04. 2025 | Lecture | Temporal Logic - Chapter 4 | Bettina | mc3-logics | hw5 |
| 08. 04. 2025 | Lecture | CTL Model Checking - Chapter 5 | Bettina | ||
| 29. 04. 2025 | Lecture | UPPAAL - MC for Timed Properties | Florian Lorber | ||
| 06. 05. 2025 | Lecture | LTL Model Checking - Chapter 7 | Bettina | ||
| 13. 05. 2025 | Lecture | LTL Model Checking - Chapter 7 + Reactive Synthesis | Bettina | ||
| 20. 05. 2025 | Lecture | Probabilistic Model Checking - Chapter 10 - PRISM & Reachability in Markov Chains | Stefan | ||
| 27. 05. 2025 | Lecture | Probabilistic Model Checking – Chapter 10 – PCTL and MDPs | Stefan | ||
| 03. 06. 2025 | Lecture | Statistical Model Checking | Bettina | ||
| 17. 06. 2025 | Lecture | Security Verification | Roderick | ||
| 24. 06. 2025 | Exam |
Practicals Schedule
| Date | Type | Topic | Lecturer | Material |
|---|---|---|---|---|
| 04.03.2025 13:45 - 14:30 | Lecture | Intro (merged with lecture) | Roderick | |
| 11.03.2025 13:45 - 14:30 | Handout | Warmup Exercise | Johannes | |
| 18.03.2025 13:45 - 14:30 | Tutorial | Introduction to Z3 | Johannes | |
| 25.03.2025 13:45 - 14:30 | Handout | BMC Exercise | Johannes | |
| 01.04.2025 13:45 - 14:30 | Question Hour | Warmup Exercise | Johannes | |
| 06.04.2025 23:59 Online | Deadline | Warmup Deadline | --- | |
| 08.04.2025 13:45 - 14:30 | Tutorial | Hardware and Verilog | Johannes | |
| 06.05.2025 13:45 - 14:30 | Handout | K-Induction Exercise | Johannes | |
| 13.05.2025 13:45 - 14:30 | Question Hour | Question Hour BMC | Johannes | |
| 25.05.2025 23:59 Online | Deadline | BMC Deadline | ||
| 03.06.2025 13:45 - 14:30 | Question Hour | Question Hour K-Induction | Johannes | |
| 08.06.2025 23:59 Online | Deadline | K-Induction Deadline | --- |
Communication and Venue
Lecture and practicals are both on campus. However, we also encourage students to join the #MC channel (🤖) on the official ISEC Discord server, where you can talk with other students, ask us questions about the courses and get updates.Lecture Dates
| Date | Begin | End | Location | Event | Type | Comment |
|---|---|---|---|---|---|---|
| 2025/04/08 | 12:00 | 13:45 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VO | fix/ |
| 2025/04/08 | 13:45 | 14:30 | HS i11 "SIEMENS Hörsaal" | Abhaltung | UE | fix/ |
| 2025/04/29 | 12:00 | 13:45 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VO | fix/ |
| 2025/04/29 | 13:45 | 14:30 | HS i11 "SIEMENS Hörsaal" | Abhaltung | UE | fix/ |
| 2025/05/06 | 12:00 | 13:45 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VO | fix/ |
| 2025/05/06 | 13:45 | 14:30 | HS i11 "SIEMENS Hörsaal" | Abhaltung | UE | fix/ |
| 2025/05/13 | 12:00 | 13:45 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VO | fix/ |
| 2025/05/13 | 13:45 | 14:30 | HS i11 "SIEMENS Hörsaal" | Abhaltung | UE | fix/ |
| 2025/05/20 | 12:00 | 13:45 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VO | fix/ |
| 2025/05/20 | 13:45 | 14:30 | HS i11 "SIEMENS Hörsaal" | Abhaltung | UE | fix/ |
| 2025/05/27 | 12:00 | 13:45 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VO | fix/ |
| 2025/05/27 | 13:45 | 14:30 | HS i11 "SIEMENS Hörsaal" | Abhaltung | UE | fix/ |
| 2025/06/03 | 12:00 | 13:45 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VO | fix/ |
| 2025/06/03 | 13:45 | 14:30 | HS i11 "SIEMENS Hörsaal" | Abhaltung | UE | fix/ |
| 2025/06/17 | 12:00 | 13:45 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VO | fix/ |
| 2025/06/17 | 13:45 | 14:30 | HS i11 "SIEMENS Hörsaal" | Abhaltung | UE | fix/ |
| 2025/06/24 | 12:00 | 13:45 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VO | fix/ |
| 2025/06/24 | 13:45 | 14:30 | HS i11 "SIEMENS Hörsaal" | Abhaltung | UE | fix/ |
