Model Checking (SS 2023)

Course Number 705080 | Sommersemester 2023

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

Administrative Information

Lecture

There are two ways to get a grade for the lecture: you do the homework or you take an exam. If you do the homework, you will get a grade for the course. To get a passing grade, you can skip at most two homework exercises. You get a 0-10 mark as the average of all  homework exercises. Non-handed exercises count as 0 points for the average. From the 0-10 mark, the final grades are distributed as follows:
Points Grade
< 5 5
5 - 6.24 4
6.25 - 7.49 3
7.5 - 8.74 2
8.75 - 10 1
Homework is done in groups of one or two persons. When you submit your homework (per email), be sure to include the names and immatriculation numbers of all group members. If you don't want to do the homework or you get a failing grade for the homework, you can do a regular exam. Please let us know when you want the exam!

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! Time slots for the practicals that are not in the schedule below, will be used for question hours!

Schedule

Date Type Topic Lecturer Slides Homework
09.03.2023 16:00-18:00 IFEG042 Lecture Intro Roderick mc01-intro
16.03.2023 16:00-18:00 IFEG042 Lecture Modeling Systems - Chapter 3 Roderick mc03-modeling homework 1
16.03.2023 18:00-19:00 IFEG042 Handout Warmup Assignment Vedad playground-12 assignment1-v1.1
23.03.2023 16:00-18:00 IFEG042 Lecture SAT-Based Model Checking (BMC, k-induction) - Chapter 10 Vedad mc10-satbasedmc1 homework 2
23.03.2023 18:00-19:00 IFEG042 Tutorial Z3 Introduction Vedad playground-34
30.03.2023 16:00-18:00 IFEG042 Lecture SAT-Based Model Checking (interpolation) -Chapter 10 Roderick mc10-satbasedmc2 homework 3
30.03.2023 18:00-19:00 IFEG042 Handout BMC Assignment Vedad assignment2
09.04.2023 23:59 Online Deadline Warmup Assignment points-assignment1
20.04.2023 16:00-18:00 IFEG042 Lecture SAT-Based Model Checking (PDR) - Chapter 10 Roderick mc10-satbasedmc3 PDR homework 4
20.04.2023 18:00-19:00 IFEG042 Tutorial Modelling with Yosys, BTOR Vedad playground-5
27.04.2023 16:00-18:00 HSi11 Lecture Temporal Logic - Chapter 4 Bettina mc04_temp_logic homework 5
27.04.2023 18:00-19:00 IFEG042 Handout K-induction Assignment Vedad Stefan assignment3
04.05.2023 16:00-18:00 IFEG042 Lecture CTL Model Checking - Chapter 5 Bettina mc05_ctl_mc homework 6
07.05.2023 23:59 Online Deadline BMC Assignment points-assignment2 deduction-assignment2
11.05.2023 16:00-18:00 IFEG042 Lecture CTL Model Checking - Chapter 5 Bettina mc07_ltl_mc homework_7
21.05.2023 23:59 Online Deadline K-induction Assignment deduction-assignment3 points-assignment3 points-final
25.05.2023 16:00-18:00 IFEG042 Lecture LTL Model Checking -Chapter 7 Bettina mc07_ltl_mc mc_shielding homework 8
01.06.2023 16:00-18:00 IFEG042 Lecture Probabilistic Model Checking - Chapter 10 - PRISM & Reachability in Markov Chains Stefan ProbMC_PRISM_MarkovChains_Reachability Homework 9
15.06.2023 16:00-18:00 IFEG042 Lecture Probabilistic Model Checking - Chapter 10 - PCTL and MDPs Stefan ProbMC_PCTL_MDPs Homework 10
22.06.2023 16:00-18:00 IFEG042 Lecture Probabilistic Model Checking - Chapter 10 - TBD Stefan ProbMC_PCTLstar_SMGs Homework 11
29.06.2023 16:00-18:00 IFEG042 Other Research SCOS

Communication and Venue

Lecture and practicals are both on campus. However, we also encourage students to join the #MC channel (🤖) on the official IAIK Discord server, where you can talk with other students, ask us questions about the courses and get updates.

Lecturers

Roderick Bloem
Roderick
Bloem

Professor

View more
Bettina Könighofer
Bettina
Könighofer

Assistant Professor

View more
Vedad Hadžić
Vedad
Hadžić

PhD Candidate

View more