[Christian-Albrechts-Universität] [Technical Faculty]

Model Checking
Seminar im Wintersemester 2004/05

Vorbesprechung: Freitag, 22. Oktober 2004 im Diplomandenraum bei uns am Lehrstuhl (erster Freitag im Semester)
  Wer in der vorlesungsfreien Zeit bereits ein Thema haben will, soll vorher vorbeikommen
Termin: Freitags, 10 ct
Beginn: n.V.
Ort: siehe Univis
Dozent: Willem-Paul de Roever und Mitarbeiter

Die vollständigen studientechnischen Daten sind über das Univis-System zu erfragen.

Bei Fragen zum Kurs, email an Harald Fecher oder Martin Steffen.



Modelchecking ist eine Technik zur Verifikation von endlichen und zunehmend auch unendlichen Systemen. Im Gegensatz zu Theorembeweisern oder gar ``Papier-und-Bleistift-Verifikationen'' zielen sie auf eine automatische Überprüfung von Eigenschaften eines Systems. Dies erklärt die zunehmende Akzeptanz von Modelcheckern in der Industrie. In bestimmten Bereichen, speziell bei der Hardwareverifikation und dem Chipentwurf, wird Modelchecking mittlerweile routinemäßig als Teil des Entwurfszyklus eingesetzt. Als Disziplin verbindet es die Gebiete der mathematischen Logik mit algorithmischen Fragen nach effizienten Suchstrategien, adäquater Maschinenrepräsentierung und anderem mehr.

Aufbauend auf die Vorlesung des Sommersemesters 4 werden im Seminar ausgewählten Kapitel aus den Büchern Model Checking [1] und Lamports Specifying Systems [2] behandelt.

Themen(bereiche) für Vorträge sind:

Scheinkriterium

Verlangt ist die Ausarbeitung (mit Hilfestellung natürlich) und die Präsentation eines Vortrages über das gewählte Thema. Relevant sind Die Reihenfolge und die genauen Termine werden zu Beginn des Semesters festgelegt.

Vorträge

  Termin Vortragender Thema
  26.November 2004 Carsten Krapp CTL Modelchecking
  28.1.05 Andreas Tonder Mu-Kalkül

Table 1: Vorträge

Links

References

[1]
E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.

[2]
L. Lamport. Specifying Systems. The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002.
Pages last (re-)generated January 28, 2005
This document was translated from LATEX by HEVEA.