Model Checking

Course Number 705080 and 705081 | 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

Administrative Information

Lecture and exercises (both possible virtual)

Lecture Dates

Date Begin End Location Event Type Comment
2021/03/09 10:00 12:00 Seminarraum IGI Abhaltung VO fix/
2021/03/09 12:00 13:00 Seminarraum IGI Abhaltung UE fix/
2021/03/16 10:00 12:00 Seminarraum IGI Abhaltung VO fix/
2021/03/16 12:00 13:00 Seminarraum IGI Abhaltung UE fix/
2021/03/23 10:00 12:00 Seminarraum IGI Abhaltung VO fix/
2021/03/23 12:00 13:00 Seminarraum IGI Abhaltung UE fix/
2021/04/13 10:00 12:00 Seminarraum IGI Abhaltung VO fix/
2021/04/13 12:00 13:00 Seminarraum IGI Abhaltung UE fix/
2021/04/20 10:00 12:00 Seminarraum IGI Abhaltung VO fix/
2021/04/20 12:00 13:00 Seminarraum IGI Abhaltung UE fix/
2021/04/27 10:00 12:00 Seminarraum IGI Abhaltung VO fix/
2021/04/27 12:00 13:00 Seminarraum IGI Abhaltung UE fix/
2021/05/04 10:00 12:00 Seminarraum IGI Abhaltung VO fix/
2021/05/04 10:00 12:00 Seminarraum IGI Abhaltung VO fix/
2021/05/04 12:00 13:00 Seminarraum IGI Abhaltung UE fix/
2021/05/04 12:00 13:00 Seminarraum IGI Abhaltung UE fix/
2021/05/11 10:00 12:00 Seminarraum IGI Abhaltung VO fix/
2021/05/11 12:00 13:00 Seminarraum IGI Abhaltung UE fix/
2021/05/18 10:00 12:00 Seminarraum IGI Abhaltung VO fix/
2021/05/18 12:00 13:00 Seminarraum IGI Abhaltung UE fix/
2021/06/01 10:00 12:00 Seminarraum IGI Abhaltung VO fix/
2021/06/01 12:00 13:00 Seminarraum IGI Abhaltung UE fix/
2021/06/08 10:00 12:00 Seminarraum IGI Abhaltung VO fix/
2021/06/08 12:00 13:00 Seminarraum IGI Abhaltung UE fix/
2021/06/15 10:00 12:00 Seminarraum IGI Abhaltung VO fix/
2021/06/15 12:00 13:00 Seminarraum IGI Abhaltung UE fix/
2021/06/22 10:00 12:00 Seminarraum IGI Abhaltung VO fix/
2021/06/22 12:00 13:00 Seminarraum IGI Abhaltung UE fix/

Lecturers

Roderick Bloem
Roderick
Bloem

Professor

View more