Model Checking

Semester:

WS 2012/2013

Modul:

CS4138

Lecturer:

Assistants:

Model checking comprises a set of techniques for the automatic verification of reactive systems. The properties to be checked are specified as formulas in different versions of temporal logic. Basically, there are two different approaches: The first approach systematically analyses the state space of the system; the second approach uses finite automata and algorithms known from automata theory. Naive implementations of these ideas, however, are inefficient and impractical. In recent years, various clever data structures and algorithms have been developed, which render model checking a practical relevant issue. Today, model checking is is applied in saftety critical systems and hardware design in order to detect faulty design as early as possible in the design process. This course introduces the basic concepts of model checking and the techniques which help to make model checking more efficient.

WS 2012/2013

Lecture
Monday 15:30-18:00 Gebäude 64/OG 1/108 (Seminarraum ISP) (not every week)
Tuesday 16:00-19:00 Gebäude 64/OG 1/108 (Seminarraum ISP) (not every week)
Thursday 19:00-21:00 Gebäude 64/OG 1/108 (Seminarraum ISP) (not every week)
Friday 12:00-16:30 Gebäude 64/OG 2/2035 (Seminarraum IFIS) (not every week)

Exercise
Tuesday 12:30-14:00 Gebäude 64, OG 2/2035 (IFIS) (not every week)

click to view Dates.

Lecture

Dates

Lectures will be held block-wise on Friday afternoons. Check the dates above for a preliminary schedule. Note, there will be no lecture on November 2, 2012!

Mailing List

Participants can subscribe to the model checking mailing list. The list serves for internal announcements
and discussions.

Prerequisites

Participants should have a basic knowledge of logic.

References and further reading

E. M. Clarke, O. Grumberg, D. A. Peled: Model Checking. MIT Press, 1999.
M. Hofmann, M. Lange: Automatentheorie und Logik. Springer, 2011.
Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, MIT Press 2008

Intended audience

Wahlplichtmodul Master Informatik, 3. Semester, Schwerpunktfach Software Systems Engineering Wahlplichtmodul Master Informatik, 3. Semester, Vertiefungsblock Programmierung

Exercises

See the dates above for a preliminary schedule.

Students are encouraged to solve the exercises and attend discussions. Solutions can be handed in for correction and feedback. Note that exercise topics may be subject to examination.

The Exercises will not necessarily be discussed entirely. Please ask for discussion on specific topics (e.g. repetition of lecture topics), if desired.

Do not hesitate to contact Normann Decker for further questions.

Material