Temporale Logik: Model Checking

Prof. R. Ramanujam

Bereich: III, Vorlesung: 2 Std.

Zeit & Ort: Mittwoch, 12.00 - 13.30 Uhr, Raum 2770

Beginn 3.5.2000

Übung: keine

Lernziele: During the nineties, formal verification has seen the advent of algorithmic techniques, principally that of  model checking. Here, the focus has shifted away from proofs of  correctness to finding usually elusive bugs, from verifying ``code'' to verifying `design'. A number of tools have been built recently, and used principally in  hardware verification. This course is an attempt to introduce model checking in temporal logics and highlight the problems involved.

Hörerkreis: Studierende der Informatik und Mathematik

Note: The lectures are taught in English.

Voraussetzungen: Vordiplom

Empfehlenswert für: Anyone who is interested in algorithmic problems with motivation from logic.

Skript und Literatur: The course will use primarily only a set of papers as course material. The following book is recommended for reading:

Manna, Z. and Pnueli, A.,
The temporal logic of reactive and concurrent systems
Springer-Verlag, 1991.

The transparencies used in the lectures can be accessed from here. Click below for postscript files of lectures.
Lecture 1
Lecture 2
Lecture 3
Lecture 4
Lecture 5
Lecture 7

A set of lecture notes on Modal logic in computer science are available.
Lecture Notes

R. Ramanujam, 16.05.2000