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