Model Checking (SS 2022)

Course Number 705080 and 705081 | Sommersemester 2022

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.

Schedule

Date Type Topic Lecturer Slides Homework
2022-03-03  16:30-18:30 HSi13 Lecture Intro Roderick mc01-intro
2022-03-10   16:30-18:30 HSi13 Lecture Modeling Systems – Chapter 3 Roderick mc03-modeling homework1

[fixed a typo on 15 Mar]

2022-03-17   16:30-18:30 HS BE01 Lecture SAT-Based Model Checking (BMC, k-induction) – Chapter 10 Roderick mc10-satbasedmc3 MC-homework2

[fixed typo on 22 Mar]

MC-homework3-solution

2022-03-17   18:30-19:30 HS BE01 Handout Warmup Assignment Vedad assignment1
2022-03-24   14:00-16:00 HSi13 Lecture SAT-Based Model Checking (interpolation) -Chapter 10 Roderick mc10-satbasedmc-2 MC-homework3
2022-03-24   16:00-17:00 HSi13 Tutorial Z3 Introduction Vedad sudoku-z3 sqrt
2022-03-31   14:00-16:00 HSi13 Lecture SAT-Based Model Checking (PDR) – Chapter 10 Roderick mc10-satbasedmc-PDR MC-homework4
2022-03-31   16:00-17:00 HSi13 Tutorial Modelling with Yosys, BTOR Vedad demo-z3 demo
2022-04-07   14:00-16:00 HSi13 Lecture Temporal Logic – Chapter 4 Roderick mc4-logics MC-homework5
2022-04-07   16:15-17:15 HSi2 Handout BMC Assignment Vedad assignment2
2022-04-08   23:59 Online Deadline Warmup Assignment assignment1-results
2022-04-28   14:00-16:00 HSi13 Lecture CTL Model Checking – Chapter 5 Bettina CTL_MC_2022-04-28 MC-homework6
2022-05-05   14:00-16:00 HSi13 Lecture LTL Model Checking – Chapter 7 Bettina LTL_MC_Part1_2022-05-05 MC-homework_7
2022-05-05   16:00-17:00 HSi13 Handout K-induction Assignment Vedad assignment3
2022-05-06   23:59 Online Deadline BMC Assignment
2022-05-12   14:00-16:00 HSi13 Lecture LTL Model Checking -Chapter 7 Bettina LTL_MC_Part2_2022_05_12 MC-homework8_updated
2022-05-19   14:00-16:00 HSi13 Lecture Probabilistic Model Checking – Chapter 10 Bettina ProbabilisticModelCheckingOne MC_homework09
2022-05-27   23:59 Online Deadline K-induction Assignment
2022-06-02   14:00-16:00 HSi13 Lecture Software Model Checking -Chapter 14 Bettina
2022-06-09   14:00-16:00 HSi13 Lecture Probabilistic Model Checking 1 Bettina
2022-06-23   14:00-16:00 HSi13 Lecture Probabilistic Model Checking 2 Bettina
2022-06-30   14:00-16:00 HSi13 Other Research SCOS

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

Previous years: SS2021

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. Otherwise, there are 10 points per homework, 50% is a passing grade and the grades above that are divided evenly.

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 and tutorials.

Question hours regarding the assignments will be held virtually on our Discord channel on Wednesdays at 10:00.

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.

Lecture Dates

Date Begin End Location Event Type Comment
2022/06/02 14:00 16:00 HS i13 Abhaltung VO fix/
2022/06/02 16:00 17:00 HS i13 Abhaltung UE fix/
2022/06/09 14:00 16:00 HS i13 Abhaltung VO fix/
2022/06/09 16:00 17:00 HS i13 Abhaltung UE fix/
2022/06/23 14:00 16:00 HS i13 Abhaltung VO fix/
2022/06/23 16:15 17:15 HS FSI 1 "Magna Steyr Hörsaal" Abhaltung UE fix/
2022/06/30 14:00 16:00 HS i13 Abhaltung VO fix/
2022/06/30 16:00 17:00 HS i13 Abhaltung UE fix/

Lecturers

Roderick Bloem
Roderick
Bloem

Professor

View more
Bettina Könighofer
Bettina
Könighofer

Trusted AI

View more
Vedad Hadzic
Vedad
Hadzic

PhD Student

View more