Seminar in Theoretical CS, Winter Semester 2016/17

News

• 23.06.2016: we are online

Deadlines

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)

Overview

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.

Prerequisites

Basic knowledge in the following areas is expected:

• Automata theory
• Mathematical logic
• Model checking

Topics

1. • Literature: Edmund Clarke et al.: Counterexample-Guided Abstraction Refinement
   • Supervisor: Christian Dehnert
   • Student: TBA
2. • Literature: Mihaela Gheorghiu Bobaru, Corina S. Păsăreanu, Dimitra Giannakopoulou: Automated Assume-Guarantee Reasoning by Abstraction Refinement
   • Supervisor: Christian Dehnert
   • Student: TBA
3. • Literature: Jan Friso Groote, Anton Wijs: An O(m log n) Algorithm for Stuttering Equivalence and Branching Bisimulation
   • Supervisor: Sebastian Junges
   • Student: TBA
4. • Literature: Byron Cook, Heidy Khlaaf, Nir Piterman: Fairness for Infinite-State Systems
   • Supervisor: Sebastian Junges
   • Student: TBA
5. • Literature: Armin Biere et al.: Bounded model checking
   • Supervisor: Joost-Pieter Katoen
   • Student: TBA
6. • Literature: Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz: Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
   • Supervisor: Tim Lange
   • Student: TBA
7. • Literature: Arie Gurfinkel, Alexander Ivrii: Pushing to the Top
   • Supervisor: Tim Lange
   • Student: TBA
8. • Literature: Ernst Moritz Hahn et al.: Lazy Probabilistic Model Checking without Determinisation
   • Supervisor: Tim Quatmann
   • Student: TBA
9. • Literature: Radu Grosu, Scott A. Smolka: Monte Carlo Model Checking
   • Supervisor: Matthias Volk
   • Student: TBA
10. • Literature: Gavin Lowe: Concurrent depth-first search algorithms based on Tarjan's Algorithm
    • Supervisor: Matthias Volk
    • Student: TBA

Additional Material

Registration

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

Contact

Matthias Volk <matthias.volk at cs.rwth-aachen.de>