Model Checking

Overview

Lecturer: Felix Klaedtke

Classes: Mon 10-12, IFW A 34

Exercises: Mon 14-16, IFW B 42 (Christian Dax) NEW TIME!

Credits: 5

Exam: oral, 20 min, end of semester

Requirements:

Some familiarity with propositional logic, basic computational complexity theory, and basic graph algorithms is assumed. For example, you should know what a tautology is, what NP stands for, and how to find the strongly connected components of a finite graph.

Language: English

Description:

As our daily lives depend increasingly on digital systems, the reliability of these systems becomes a concern of overwhelming importance, and as the complexity of the systems grows, their reliability can no longer be sufficiently controlled by the traditional approaches of testing and simulation. Model checking concerns the use of methods for automatically verifying whether hardware or software systems meet their specifications. Over the last two decades, model checking has made enormous progress and is nowadays used in large-scale industrial applications. This course offers an introduction to the theory and practice of model checking. In particular, the course introduces temporal logics (like the branching time temporal logic CTL and the IEEE standardized temporal logic PSL) for specifying properties of concurrent systems and it will present the algorithmic core techniques of model checking (BDD-based, SAT-based, and explicit-state model checking). The course will also teach methods for coping with the state-space explosion problem (e.g., partial-order reduction and counterexample-guided-abstraction refinement). Furthermore, the course will discuss state-of-the-art tools for model checking (like SPIN and NuSMV), which will also be used in the accompanying exercise sessions.

Resources

Literature:

• Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008.
• Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. The MIT Press, 2000.