Verification and Model Checking (SS2026)
Table of Content
Content
In this course, we teach various advanced methods to verify software and hardware. Instead of classical unit tests, we present techniques for automatic detection of bugs with little user-effort to prove the correctness of a program independent of concrete input values. We will discuss model checking, 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
The practicals are split into two parts. As the first part of the practicals, 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, symbolic representations, and SMT solvers. Afterwards, we use these building blocks to implement the bounded model checking (BMC) and K-Induction algorithms you will learn in the lecture. The second part will consist of 8 pen-and-paper assignments. These assignments will consist of examples covering algorithms discussed in the lecture. You can find more details for the practicals below.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.
SLAM
T. Ball, S. K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs, SPIN 2000 Workshop on Model Checking of Software, LNCS 1885, pp. 113-130, August/September 2000.
T. Ball, S. K. Rajamani, Automatically Validating Temporal Safety Properties of Interfaces, SPIN 2001, Workshop on Model Checking of Software, LNCS 2057, pp. 103-122, May 2001.
T. Thomas Ball, Rupak Majumdar, Todd Millstein, and Sriram K. Rajamani. Automatic Predicate Abstraction of C Programs, In Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation (PLDI '01). ACM, New York, NY, USA, 203-213, 2001.
Administrative Information
Lecture
The lecture part of the course will take place in lecture hall i11. Attendance at lectures is compulsory. Exceptions may be granted for justified reasons (e.g., illness). If you cannot attend class, please reach out to us via mail.| Date | Type | Topic | Lecturer | Slides | Homework |
|---|---|---|---|---|---|
| 03. 03. 2026 | Lecture | Intro | Roderick | Slides | |
| 10. 03. 2026 | Lecture | SAT-Based Model Checking (BMC, k-induction) - Chapter 10 | Roderick | Modelling BMC | |
| 17. 03. 2026 | Lecture | SAT-Based Model Checking (Interpolation) - Chapter 10 | Roderick | ||
| 24. 03. 2026 | Lecture | SAT-Based Model Checking (PDR) - Chapter 10 | Roderick | ||
| 14. 04. 2026 | Lecture | SLAM I | Roderick | ||
| 21. 04. 2026 | Lecture | SLAM II | Roderick | ||
| 28. 04. 2026 | Lecture | SLAM III | Roderick | ||
| 05. 05. 2026 | Lecture | Security Verification | Roderick | ||
| 12. 05. 2026 | Lecture | Temporal Logic | Bettina | ||
| 19. 05. 2026 | Lecture | CTL MC | Bettina | ||
| 02. 06. 2026 | Lecture | LTL MC | Bettina | ||
| 09. 06. 2026 | Lecture | LTL MC | Bettina | ||
| 16. 06. 2026 | Lecture | Probabilistic MC | Stefan | ||
| 23. 06. 2026 | Lecture | Probabilistic MC | Stefan |
Practicals
Assignments Sheets
The repository for the programming tasks will be released via this repository. The pen-and-paper assignments will be released via the table below.Submission of Programming Assignments
Programming assignments will be submitted via git. You will receive your repository after the registration deadline for the course has passed. The first and second programming assignments will be graded based on your submitted code. You may also be randomly picked for an assignment interview for either the first or second programming assignment.
Practical Groups for Pen-and-Paper Assignments
The pen-and-paper assignments will be discussed in live blackboard sessions during class. Please register for one of the six groups via TUGonline. Students are required to indicate the tasks they have solved in TeachCenter by Monday, 23:59, prior to the respective session. During the practical, students who marked a task as solved may be randomly selected to present their solution at the blackboard.
Marking a task as solved in TeachCenter constitutes registration for examination in the practical session.
Absence from Practical Classes
Attendance at practical classes is compulsory. Exceptions may be granted for justified reasons (e.g., illness). In such cases, students must tick and upload their solutions on time (according to the assignment deadline) and present them in a replacement interview, which will be held the following Monday.
| Date | Type | Topic | Lecturer | Material |
|---|---|---|---|---|
| 03.03.2026 | Lecture | Introduction | Stefan | Slides Assignment Sheet |
| 10.03.2026 | Handout | BMC | Stefan | |
| 17.03.2026 | Question Hour | BMC | Stefan | |
| 23.03.2026 23:59 Online | Deadline | Deadline - BMC | --- | |
| 24.03.2026 | Handout | K-Induction | Stefan | |
| 21.04.2026 23:59 Online | Deadline | Deadline - K-Induction | ||
| 27.04.2026 | Class | SLAM | Tutors | |
| 04.05.2026 | Class | SLAM | Tutors | |
| 11.05.2026 | Class | Security Verification | Tutors | |
| 18.05.2026 | Class | Temporal Logic | Tutors | |
| 01.06.2026 | Class | CTL MC | Tutors | |
| 08.06.2026 | Class | LTL MC | Tutors | |
| 15.06.2026 | Class | LTL MC | Tutors | |
| 22.06.2026 | Class | Probabilistic MC | Tutors |
Grade
-
Programming Assignments 1 (P1): 20 points
-
Programming Assignments 2 (P2): 15 points
- Pen-and-Paper Assignments 1–8 (PP1-8): 8 × 12.5 points
| Total Points | Grade |
| < 50 | 5 |
| 50 - 62.4 | 4 |
| 62.5 - 74.9 | 3 |
| 75 - 87.4 | 2 |
| 87.5 - 100 | 1 |
Communication and Venue
Lecture and practicals are both on campus. However, we also encourage students to join the #VMC channel (🤖) on the official ISEC Discord server, where you can talk with other students, ask us questions about the courses and get updates.Usage of Generative AI
We follow the general TU Graz guidelines on the use of generative AI.
Lecture Dates
| Date | Begin | End | Location | Event | Type | Comment |
|---|---|---|---|---|---|---|
| 2026/03/19 | 08:00 | 10:00 | HS i7 | Abhaltung | VU | fix/ |
| 2026/03/24 | 12:00 | 14:00 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VU | fix/ |
| 2026/03/24 | 17:00 | 18:00 | HS i9 | Abhaltung | VU | fix/Übungsteil |
| 2026/03/24 | 17:00 | 18:00 | HS i9 | Abhaltung | VU | fix/ |
| 2026/04/14 | 12:00 | 14:00 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VU | fix/ |
| 2026/04/21 | 12:00 | 14:00 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VU | fix/ |
| 2026/04/27 | 10:00 | 11:00 | Seminarraum IGI | Abhaltung | VU | fix/ |
| 2026/04/27 | 10:00 | 11:00 | Seminarraum CGV | Abhaltung | VU | fix/ |
| 2026/04/27 | 10:00 | 11:00 | Franz Leberl Seminarraum | Abhaltung | VU | fix/ |
| 2026/04/27 | 10:00 | 11:00 | HS i5 | Abhaltung | VU | fix/ |
| 2026/04/27 | 11:00 | 12:00 | Seminarraum CGV | Abhaltung | VU | fix/ |
| 2026/04/27 | 11:00 | 12:00 | Seminarraum IGI | Abhaltung | VU | fix/ |
| 2026/04/27 | 11:00 | 12:00 | Franz Leberl Seminarraum | Abhaltung | VU | fix/ |
| 2026/04/27 | 11:00 | 12:00 | HS i5 | Abhaltung | VU | fix/ |
| 2026/04/28 | 12:00 | 14:00 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VU | fix/ |
| 2026/05/04 | 10:00 | 11:00 | Seminarraum IGI | Abhaltung | VU | fix/ |
| 2026/05/04 | 10:00 | 11:00 | Seminarraum CGV | Abhaltung | VU | fix/ |
| 2026/05/04 | 10:00 | 11:00 | Franz Leberl Seminarraum | Abhaltung | VU | fix/ |
| 2026/05/04 | 10:00 | 11:00 | HS i5 | Abhaltung | VU | fix/ |
| 2026/05/04 | 11:00 | 12:00 | Seminarraum CGV | Abhaltung | VU | fix/ |
| 2026/05/04 | 11:00 | 12:00 | Seminarraum IGI | Abhaltung | VU | fix/ |
| 2026/05/04 | 11:00 | 12:00 | Franz Leberl Seminarraum | Abhaltung | VU | fix/ |
| 2026/05/04 | 11:00 | 12:00 | HS i5 | Abhaltung | VU | fix/ |
| 2026/05/05 | 12:00 | 14:00 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VU | fix/ |
| 2026/05/11 | 10:00 | 11:00 | Seminarraum IGI | Abhaltung | VU | fix/ |
| 2026/05/11 | 10:00 | 11:00 | Seminarraum CGV | Abhaltung | VU | fix/ |
| 2026/05/11 | 10:00 | 11:00 | Franz Leberl Seminarraum | Abhaltung | VU | fix/ |
| 2026/05/11 | 10:00 | 11:00 | HS i5 | Abhaltung | VU | fix/ |
| 2026/05/11 | 11:00 | 12:00 | Franz Leberl Seminarraum | Abhaltung | VU | fix/ |
| 2026/05/11 | 11:00 | 12:00 | Seminarraum CGV | Abhaltung | VU | fix/ |
| 2026/05/11 | 11:00 | 12:00 | HS i5 | Abhaltung | VU | fix/ |
| 2026/05/11 | 11:00 | 12:00 | Seminarraum IGI | Abhaltung | VU | fix/ |
| 2026/05/12 | 12:00 | 14:00 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VU | fix/ |
| 2026/05/18 | 10:00 | 11:00 | Seminarraum IGI | Abhaltung | VU | fix/ |
| 2026/05/18 | 10:00 | 11:00 | Seminarraum CGV | Abhaltung | VU | fix/ |
| 2026/05/18 | 10:00 | 11:00 | Franz Leberl Seminarraum | Abhaltung | VU | fix/ |
| 2026/05/18 | 10:00 | 11:00 | HS i5 | Abhaltung | VU | fix/ |
| 2026/05/18 | 11:00 | 12:00 | Franz Leberl Seminarraum | Abhaltung | VU | fix/ |
| 2026/05/18 | 11:00 | 12:00 | Seminarraum CGV | Abhaltung | VU | fix/ |
| 2026/05/18 | 11:00 | 12:00 | Seminarraum IGI | Abhaltung | VU | fix/ |
| 2026/05/18 | 11:00 | 12:00 | HS i5 | Abhaltung | VU | fix/ |
| 2026/05/19 | 12:00 | 14:00 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VU | fix/ |
| 2026/06/01 | 10:00 | 11:00 | Seminarraum IGI | Abhaltung | VU | fix/ |
| 2026/06/01 | 10:00 | 11:00 | Seminarraum CGV | Abhaltung | VU | fix/ |
| 2026/06/01 | 10:00 | 11:00 | Franz Leberl Seminarraum | Abhaltung | VU | fix/ |
| 2026/06/01 | 10:00 | 11:00 | HS i5 | Abhaltung | VU | fix/ |
| 2026/06/01 | 11:00 | 12:00 | Franz Leberl Seminarraum | Abhaltung | VU | fix/ |
| 2026/06/01 | 11:00 | 12:00 | Seminarraum CGV | Abhaltung | VU | fix/ |
| 2026/06/01 | 11:00 | 12:00 | Seminarraum IGI | Abhaltung | VU | fix/ |
| 2026/06/01 | 11:00 | 12:00 | HS i5 | Abhaltung | VU | fix/ |
| 2026/06/02 | 12:00 | 14:00 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VU | fix/ |
| 2026/06/08 | 10:00 | 11:00 | Seminarraum IGI | Abhaltung | VU | fix/ |
| 2026/06/08 | 10:00 | 11:00 | Seminarraum CGV | Abhaltung | VU | fix/ |
| 2026/06/08 | 10:00 | 11:00 | Franz Leberl Seminarraum | Abhaltung | VU | fix/ |
| 2026/06/08 | 10:00 | 11:00 | HS i5 | Abhaltung | VU | fix/ |
| 2026/06/08 | 11:00 | 12:00 | Franz Leberl Seminarraum | Abhaltung | VU | fix/ |
| 2026/06/08 | 11:00 | 12:00 | Seminarraum CGV | Abhaltung | VU | fix/ |
| 2026/06/08 | 11:00 | 12:00 | Seminarraum IGI | Abhaltung | VU | fix/ |
| 2026/06/08 | 11:00 | 12:00 | HS i5 | Abhaltung | VU | fix/ |
| 2026/06/09 | 12:00 | 14:00 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VU | fix/ |
| 2026/06/15 | 10:00 | 11:00 | Seminarraum IGI | Abhaltung | VU | fix/ |
| 2026/06/15 | 10:00 | 11:00 | Seminarraum CGV | Abhaltung | VU | fix/ |
| 2026/06/15 | 10:00 | 11:00 | Franz Leberl Seminarraum | Abhaltung | VU | fix/ |
| 2026/06/15 | 10:00 | 11:00 | HS i5 | Abhaltung | VU | fix/ |
| 2026/06/15 | 11:00 | 12:00 | Franz Leberl Seminarraum | Abhaltung | VU | fix/ |
| 2026/06/15 | 11:00 | 12:00 | Seminarraum CGV | Abhaltung | VU | fix/ |
| 2026/06/15 | 11:00 | 12:00 | Seminarraum IGI | Abhaltung | VU | fix/ |
| 2026/06/15 | 11:00 | 12:00 | HS i5 | Abhaltung | VU | fix/ |
| 2026/06/16 | 12:00 | 14:00 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VU | fix/ |
| 2026/06/22 | 10:00 | 11:00 | Seminarraum IGI | Abhaltung | VU | fix/ |
| 2026/06/22 | 10:00 | 11:00 | Seminarraum CGV | Abhaltung | VU | fix/ |
| 2026/06/22 | 10:00 | 11:00 | Franz Leberl Seminarraum | Abhaltung | VU | fix/ |
| 2026/06/22 | 10:00 | 11:00 | HS i5 | Abhaltung | VU | fix/ |
| 2026/06/22 | 11:00 | 12:00 | Franz Leberl Seminarraum | Abhaltung | VU | fix/ |
| 2026/06/22 | 11:00 | 12:00 | Seminarraum CGV | Abhaltung | VU | fix/ |
| 2026/06/22 | 11:00 | 12:00 | Seminarraum IGI | Abhaltung | VU | fix/ |
| 2026/06/22 | 11:00 | 12:00 | HS i5 | Abhaltung | VU | fix/ |
| 2026/06/23 | 12:00 | 14:00 | HS i11 "SIEMENS Hörsaal" | Abhaltung | VU | fix/ |
