Model Checking (WS 2011/12)

Semester:

WS 2011/2012

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 2011/2012

Vorlesung
Friday 12:15-13:45 Seminarraum IFIS 2035

click to view Dates.

Lecture

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.

Intended audience:

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

Exercises

Regarding the organisation of exercises, we will try to find an agreement among all participants in the first lecture. Decissions will be announced here.

Do not hesitate to contact Normann Decker for further questions.

Search form

You are here

Model Checking (WS 2011/12)

Lecture

Exercises