**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