Model-Checking SS 2011

News | Basic information | Content | Exercises | Slides | Links

Model-Checking (also in German: Modellprüfung) is a technique for automatic verification of hardware and software systems. Given a such system and a correctness specification, a model checker checks if the system works correctly.

Prerequisites: Basic discrete math and logic.

Lecture 1: May 2

Basic introduction.

Lecture 2: May 3

Programs, computations, reachability and termination properties.
Concrete enumerative stateful reachability algorithm. See lecture notes.

Lecture 3: May 9

First order theory of (integer) linear arithmetic, symbolic representation of program states, existential quantifier elimination, and (Forward)-Symbolic-Reachability algorithm.

Tutorial 2: May 10

Syntax and semantics of first order theory of (integer) linear arithmetic, and Forward-Symbolic-Reachability algorithm. See tutorial outline.

Lecture 4: May 13

Limitations of the (Forward)-Symbolic-Reachability algorithm by example, and predicate abstraction as solution. See lecture notes.

Lecture 7: May 23

Relational composition operator and properties, abstraction refinement by interpolation, Abstract Reachability with Predicate Abstraction algorithm. See lecture notes.

Lectures 9 and 10: June 6

Simple model checker: ab implementation of the Abstract Reachability algorithm in Prolog.

Lecture 11: June 7

Modifications to simple model checker, ranking functions, automatic generation of ranking functions. See lecture notes.