Klaus Dräger

Reactive Systems Group Universität des Saarlandes Phone: +49 681 302 5613 Fax: +49 681 302 5636 eMail: draeger at cs.uni-sb.de Building: E 1.3 Room: 508

About me

I defended my Ph.D. thesis in August, 2010. Currently, I am working as a researcher at the University of Oxford. My research interests are model checking and verification of complex real-time systems.

Research

Verification of complex concurrent real-time systems is a challenging topic. In order to prove that a given system satisfies a desired property, one needs to deal with an infinite state space (due to the real-time aspect and infinite data domains) as well as a complex control structure (due to the parallelism between the system components.)

Abstraction refinement is a highly effective method for dealing with infinite state spaces. In this approach, a finite-state abstraction of the system is constructed in such a way that if the abstraction is correct, then so is the system. If the abstraction exhibits an error, then either this error also exists in the concrete system, or it can be removed by a suitable refinement of the abstraction. In our paper Slicing Abstractions, we introduced a new model-based refinement loop that incorporates local refinements and slicing operations in order to obtain much smaller and more focused abstractions.

Since the complex control structure of highly concurrent systems makes reasoning about such systems hard, there is a lot of interest in compositional methods, by which one can derive properties of individual components which can be used to reason about the system as a whole. We recently introduced subsequence invariants, a class of invariants of the possible sequences of synchronization events in a system, which can be efficiently computed for each process and yet hold for the entire system.

Publications