Advances in Model Checking

Seminar in Theoretical CS, Winter Semester 2016/17


  • 23.06.2016: we are online


27.10.2016, 14:00 Kick-off meeting at seminar room of i2 (E1, room 4201b)
21.11.2016 Detailed outline of report due
19.12.2016 Seminar report due
09.01.2016 Presentation slides due
19.01.2016 Seminar talks at seminar room of i2 (E1, room 4201b)


Model checking is an automatic verification technique for both software and hardware systems. It systematically checks if a given model representing the system satisfies a property (e.g. a safety requirement) and therefore verifies if a system fulfills the desired behavior.

This seminar aims to give an overview of the current research in the field of model checking. Each topic is covered by a scientific journal or conference article. These research articles are the basis on which students have to prepare their report and presentation. The presentations will be given at the end of the lecture period as a block seminar.


Basic knowledge in the following areas is expected:

  • Automata theory
  • Mathematical logic
  • Model checking


Additional Material


Registration to the seminar is handled between June 24 and July 10, 2016, via the central online form.


Matthias Volk <matthias.volk at>