Model Checking

Course Number 705080 | Sommersemester 2021

Content

Model checking is a widely used technique for automatic verification and debugging for both software and hardware, with the power to revel 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, that is, what are its underlying principles?

This is the focus of this course! We will show that model checking is based on well-known paradigms from automata theory, graph algorithms, logic, and data structures. Since model checking is based on checking models, we first start by explaining what models are. Following, 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.

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

 

Schedule

Videos can be found here: https://seafile.iaik.tugraz.at/d/474b6fd4d1e34723ab77/. You can find the password on our discord server.

 

DATE TOPIC Teams Slides Homework Video
2021-03-04 Intro link mc01-intro2
2021-03-11 Chapter 3 link mc03-modeling homework_1 video
2021-03-18 Chapter 10 link mc10-satbasedmc

mc10-satbasedmc

MC-homework2 video
2021-03-25 Chapter 10 link mc10-satbasedmc2 MC-homework3. Errata: Deadline 8 April. solutions

assignment1 v1.1

video
2021-04-15 Chapter 10 link mc10-satbasedmc3 MC-homework4

hw_4a_solutions

hw4b_solutions

video
2021-04-22 Chapter 4 link mc04_temporalLogic MC-homework5

assignment2 – deadline extended to 04.06.

video
2021-04-29 Chapter 4 link mc04_temporalLogic-part2 MC-homework_6

homework6_solutions

video
2021-05-06 Chapter 5 link mc05_ctl-mc MC-homework_7 video
2021-05-20 Chapter 7 link Mc07_ltl_mc_part1 MC-homework_8 video
2021-05-27 Chapter 7 link M07_ltl_mc_part2 MC-homework_9 video
2021-06-10 Chapter 7 link Mc07_ltl_mc_part3 MC_homework_10 video
2021-06-17 Chapter 8 link mc08-bdds MC-homework11 video
2021-06-24 Chapter 12 link mcFinal-synthesis no homework video


Administrative Information

Homework

There are two ways to get a grade for the exam: 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 homeworks. Otherwise, there are 10 points per homework, 50% is a passing grade and the grades above that are divided evenly.

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 me know when you want the exam!

 

 

Lecture and exercises (both virtual)

 

IGNORE EVERYTHING BELOW THIS LINE!

Lecturers

Roderick Bloem
Roderick
Bloem

Professor

View more