Model Checking (WS 2014/15)

Semester:

WS 2014/2015

Modul:

CS4138,

CS4138SJ14,

CS4138 TSJ14,

CS4507

Lecturer:

Prof. Dr. Martin Leucker

Assistants:

Grigory Markin , Jannis Harder

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 2014/2015

Vorlesung
Tuesday 12:15-13:45 Seminarraum Informatik 3 ( Karp )
Wednesday 14:15-15:45 AM S 2 (not every week)

Übung
Wednesday 14:15-15:45 AM S 2 (not every week)

click to view Dates.

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

Lectures

Lectures start on October 21, 2014 and will be held every week on Tuesdays, 12.15 - 13.45 and every two weeks on Wednesdays, 14.15 - 15.45.

Exercises

Exercise problems will be made available on this web page. We will discuss the problems roughly every two weeks, starting on November 5, 2014.

We strongly encourage participants to work on the exercise problems and hand in (even incomplete) solutions for review before their discussion. Also, feel free to contact Jannis or Grigory and request discussion/repetition of certain topics if needed.

Mailing list

Important information related to the course Model Checking will be distributed through the mailing list. Attendees are strongly encouraged to register with the list. Note that access is only possible from inside the domain uni-luebeck.de.

Mailing list Model Checking

Examination

Topics from both, lectures and exercises, will be subject to examination. We therefor strongly recommend to follow the lectures and exercises.

Exam registration from 10.02.15 (all day) until 11.02 (all day) in the secretary.

Available dates for examination: 10.03.15 and 11.03.15

Material