Lecturer: Stefan Schwoon
Tutor: Dejvuth Suwimonteerabuth

Lectures:
Thu 14:00-15:30 in Room V47.05
Thu 15:45-17:15 (every two weeks) in Room V47.05

Exercises:
Thu 15:45-17:15 (every two weeks) in Room V47.05

Intended Audience:
Students of the Master of Science program Information Technology (INFOTECH),
students of the "Diplom-Studiengang Elektrotechnik und Informationstechnik"
(under the German title "Netze und Prozesse", the lectures are identical),
students of Informatik or Softwaretechnik (Vertiefungslinie Sichere und Zuverlässige Softwaresysteme)

Contents (short version):
Modeling and analysis of parallel and distributed systems. Specifying system properties with temporal logics and using model checking to verify them. Basics of computer aided verification algorithms. Petri nets as system description formalisms.

Slides: PDF file, LaTeX sources

Tools:
The PEP tool (University of Oldenburg)
Spin (Bell Labs) -- short introduction to Promela (PDF) and models used in the lecture (ZIP)
DDcal (University of Colorado) -- a BDD "calculator"
SMV (CMU) -- some tool demonstration slides (PDF) from last year and a couple of examples (tar.gz)

Exam:
The problems (of the written exam on 15.2.2007)
Sample solutions