Model Checking

Prof. Dr. Christel Baier and Dr. Sascha Klüppelholz
SWS: (4/4/0), in English

Description

Model Checking is a fully automatic verification method for reactive systems. This course provides an introduction to the main principles of model checking:

• modeling reactive systems by transition systems
• linear time properties and Büchi automata
• linear temporal logic and automata-based model checking
• computation tree logic

and selected topics of:

• bisimulation and simulation relations
• probabilistic and timed automata
• partial order reduction, symbolic model checking

Dates

The first lecture will be held on Thursday, October 17th at 09:20 am. The date of the first tutorial will be announced in the lecture. There will be no fixed assignment of the lectures and exercises to time slots. The schedule for the lectures and tutorials will be announced every week.

The course consists of a (4/2/0) lecture with exercises for the theoretical foundations (October – December) and an introduction to model checkers with practical exercises (0/2/0) (January).

Prerequisites

For the course, basic knowledge on algorithms, complexity theory, automata theory and logic is presumed.

Creditability

Bachelor Informatik

• INF-B-510: Vertiefung in der Informatik
• INF-B-520: Vertiefung zur Bachelorarbeit

Master Informatik

• INF-BAS6: Basismodul Theoretische Informatik
• INF-VERT6: Vertiefungsmodul Theoretische Informatik

Diplom Informatik

• INF-BAS6: Basismodul Theoretische Informatik
• INF-VERT6: Vertiefungsmodul Theoretische Informatik

Master Computational Logic

• MCL-TCSL: Theoretical Computer Science and Logic

Course Material

Here, you find the slides in PDF format after each lecture.

• Part 01 (2019-10-17) PDF
• Part 02 (2019-10-18) PDF
• Part 03 (2019-10-24) PDF
• Part 04 (2019-10-25) PDF
• Part 05 (2019-11-01) PDF
• Part 06 (2019-11-08) PDF
• Part 07 (2019-11-14) PDF
• Part 08 (2019-11-15) PDF
• Part 09 (2019-11-21) PDF
• Part 10 (2019-11-22) PDF
• Part 11 (2019-11-29) PDF
• Part 12 (2019-12-05) PDF
• Part 13 (2019-12-06) PDF
• Part 14 (2019-12-12) PDF
• Part 15 (2019-12-13) PDF
• Part 16 (2019-12-19) PDF

Exercises

Here, you find the sheets for the upcoming exercise in PDF format.

• Sheet 01 (2019-10-18, discussion on 2019-10-24 and 2019-10-25) PDF
• Sheet 02 (2019-11-01, discussion on 2019-11-07 and 2019-11-08) PDF
• Sheet 03 (2019-11-08, discussion on 2019-11-15) PDF
• Sheet 04 (2019-11-15, discussion on 2019-11-21) PDF
• Sheet 05 (2019-11-22, discussion on 2019-11-28 and 2019-11-29) PDF
• Sheet 06 (2019-12-06, discussion on 2019-12-12 and 2019-12-13) PDF
• Sheet 07 (2019-12-13, discussion on 2019-12-20) PDF
• Sheet 08 (2020-01-31, discussion on 2020-02-06) PDF (old: PDF)

Practical Part

Here, you find the material for the practical part of the course.

• Practical Part 1 (2020-01-09) PDF
• Practical Part 2 (2020-01-16/17) PDF
• Exercises 1 (2020-01-09-17) PDF
• Practical Part 3 (2020-01-23/24) PDF

• Exercises 2 (2020-01-24-31) PDF

Before the first course, please prepare by visiting the  Vereofy website and download and execute Vereofy.

Literature

The course follows the book “Principles of Model Checking” (C. Baier, J.P. Katoen, Principles of Model Checking, MIT Press) closely. This book is available at the SLUB (Lehrbuchsammlung).

Mailing list

Students are advised to subscribe to the mailing list of the lecture.

Contact