Schedule

Type

Day

Time

Place

Start

Lecturer

V4

Tue

14:00-15:30

AH II

October 21

Wed

10:00-11:30

AH II

October 22

Ü2

Fr

10:00-11:30

AH II

October 31

  • On Friday, February 20, we offer a discussion at 10:00 in room 4201b to discuss questions.
  • We offer an office hour (room 4207) on Tuesday, 24.02. from 16:00 to 17:00 o'clock.
  • The list of students with at least 50% of the exercise points (admission for BSc. students) is available here (tentative, please check!).
  • Some old exams may be downloaded: exam 1 (solution) exam 2 (solution) exam 3 (solution).
  • Written examination on Friday, February 27 from 10:00 to 11:30 in AH II.
  • The results of the first exam are available. You may inspect the corrections on Monday, March 9, 16:00-17:00 o'clock in room 4201b.
  • The repetition exam is scheduled on Monday, March 30 from 10:00 to 11:30 in AH II.
  • Note the time of the repetition exam! On the day before (Sunday!), Europe switches to daylight saving time!
  • The results of the re-exam are available. You may inspect the corrections until April 30 by making an appointment (via e-mail).


News

  • In the slides for lecture 14, a typo on slide 17 where the until operator is reduced to a release formula has been fixed.


Motivation




In 2008, the ACM awarded the prestigious Turing Award - the Nobel Prize in Computer Science - to the pioneers of Model Checking: Ed Clarke, Allen Emerson, and Joseph Sifakis.

 

Why? Because model checking has evolved in the last twenty-five years into a widely used verification and debugging technique for both software and hardware.

 

It is used (and further developed) by companies and institutes such as IBM, Intel, NASA, Cadence, Microsoft, and Siemens, to mention a few, and has culminated in a series of mostly freely downloadable software tools that allow the automated verification of, for instance, C#-programs or combinational hardware circuits.

Subtle errors, for instance due to multi-threading, that remain undiscovered using simulation or peer reviewing can potentially be revealed using model checking.  Model checking is thus an effective technique to expose potential design errors and improve software and hardware reliability.

 

But how does it work, that is, what are its underlying principles?

That's exactly the focus of this lecture series!

 

We will show that model checking is based on well-known paradigms from automata theory, graph algorithms, logic, and data structures.  Its complexity is analyzed using standard techniques from complexity theory.


Contents of the lecture


Model checking is based on checking models. So, we first start by explaining what models are, and will make clear that so-called labeled transition systems, a model that is akin to automata, are suitable for modeling sequential, as well as multi-threading programs. 

This is followed by a detailed study on various classes of system properties such as safety, liveness, and fairness.  It will be shown how finite automata as well as variants thereof that accept infinite words are suitable for verifying regular properties.

The linear-time and branching time temporal logics LTL and CTL are then introduced and compared. Model checking algorithms for these logics together with detailed complexity considerations are covered. 

Finally, abstraction techniques based on bisimulation and simulation relations are covered. These techniques are at key techniques to combat the state explosion problem.


Prerequisites

This course is suitable for Hauptdiplom, bachelor (this course is part of the "Wahlkatalog" in theoretical computer science), as well as master students. 

We expect students to have some basic knowledge in:

  • Automata Theory
  • Mathematical Logic
  • Discrete Mathematics
  • Complexity Theory
  • Algorithms and Data Structures

The course book (see below) will contain a summary of the issues in these areas that are relevant to this lecture series.  We believe that this course is also well-suited for students in electrical engineeering and mathematics.


Follow-up courses

This course provides the basis for the follow-up courses:

Advanced Model Checking (planned for SS 2009)
Model Checking Labs (planned for SS 2009)

Moreover, it is related to courses such as:

  • Semantics and Verification of Software
  • Automata and Reactive Systems (i7)
  • Automata on Infinite Words (i7)
  • Formal Methods for Embedded Systems (i11)

There are thus plenty of opportunities to combine this course with others!  We also regularly offer seminars that are based on model checking and offer various master and diplom theses on model checking and its applications.


Slides and exercise sheets

Date

Lecture

Subject

Slides

Exercise Sheet

Solution

October 21

1

Introduction

October 22

2

Transition systems

October 28

3

Concurrency

October 29

4

Channel Systems

November 4

5

The State Explosion Problem

Linear-Time Properties

November 5

6

Safety and Liveness Properties

November 11

7

Fairness

November 12

8

Model Checking Regular Safety Properties

November 18

9

Büchi Automata

November 19

10

Deterministic and Generalized Büchi Automata

November 25

11

Verifying Omega-Regular Properties (I)

November 26

12

Verifying Omega-Regular Properties (II)

December 2

13

Linear Temporal Logic (I)

December 3

14

Linear Temporal Logic (II) -- updated --

December 10

15

Fairness in LTL

December 16

16

LTL model checking

December 17

17

Complexity and Correctness of LTL Model Checking

January 6

18

Computation Tree Logic

January 7

19

CTL, LTL and CTL*

January 13

20

CTL model checking

January 14

21

CTL counterexamples and CTL* model checking

January 20

22

Fairness in CTL

January 21

--

no lecture

--


January 27

23

Bisimulation

January 28

24

Bisimulation and CTL*

February 3

25

Simulation preorder

The solutions are accessible within the university network with the credentials given in the exercise class.


Materials


The lectures and all materials are in english. The slides will be made available via this webpage during the course.

 

The course is based on the recently published book:

Principles of Model Checking
by Christel Baier and Joost-Pieter Katoen
MIT Press, 2008.

An errata document to the book may be found here.


It is possible to buy a book (about 40 euros), but there is no need to do so as there are various copies of the book available at the CS library

The course will basically cover Chapters 1 through 7 (upto section 7.3).

Additional literature:

  • E.M. Clarke, O. Grumberg, D.A. Peled: Model Checking, MIT Press, 1999

  • M. Huth and M.D. Ryan: Logic in Computer Science - Modelling and Reasoning about Systems, Cambridge University Press, 2nd edition, 2004

  • K. Schneider: Verification of Reactive Systems, Springer-Verlag, Texts in Theoretical Computer Science. An EATCS Series, 2004