Seminar: Symbolic Model Checking in the Analysis of Critical Systems


Seminar: Prof. Dr. Stefan Leue, Alina Bey

Thursday 15:15 - 16:45  Room: PZ 902

SessionDateTopic Initial Meeting, Formalities, Topic Distribution How To Seminar



Model Checking is a technique to determine whether the state-transition model (Kripke structure) for some software or hardware system satisfies a given specification, typically formalized using some form of temporal logic. This seminar will present various methods, techniques and tools in the realm of symbolic model checking. In symbolic model checking, the transition system is encoded in the form of an Ordered Binary Decision Diagram (OBDD), a canoncial representation for boolean functions. This representation can then be used to either perform fixpoint-based CTL or LTL mode checking, or to translate the model into a SAT problem and to perform bounded model checking on it.


Bachelor Computer Science level standing in Logic, Theory of Computaton, Programming and Software Engineering

Subject Area

Informatik der Systeme / Angewandte Informatik 

Contents / Syllabus

The participants will be equipped with a deeper understanding of Symbolic Model Checking.

Seminar taught entirely in English.

Seminar presentation (appr. 30 mins.) and seminar report (appr. 10 pages)

The grading schemes can be found here:


Will be announced


SWS: 2
ECTS-points: 4


Basic Techniques

Timed Systems


Fixed-Point Logic

Hybrid Systems

Infinite Systems