Klaus Dräger
 |
Reactive Systems Group |
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
| [DKFW10] | Klaus Dräger, Andrey Kupriyanov, Bernd Finkbeiner, and Heike Wehrheim. SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems. TACAS 2010. |
| [BDFW08] | Ingo Brückner, Klaus Dräger, Bernd Finkbeiner, and Heike Wehrheim. Slicing Abstractions. Extended Version of [BDFW07] . Fundamenta Informaticae, 2008. |
| [DFP08] | Klaus Dräger, Bernd Finkbeiner, and Andreas Podelski. Directed Model Checking with Distance-preserving Abstractions. Extended Version of [DFP06] . Software Tools for Technology Transfer (STTT), 2008. |
| [DF08a] | Klaus Dräger and Bernd Finkbeiner.Subsequence Invariants. CONCUR 2008. |
| [DF08b] | Klaus Dräger and Bernd Finkbeiner.Subsequence Invariants. Extended Version of [DF08a] . AVACS Technical Report 42, 2008. |
| [KDHFDPB07] | Sebastian Kupferschmid, Klaus Dräger, Jörg Hoffmann, Bernd Finkbeiner, Henning Dierks, Andreas Podelski, and Gerd Behrmann. UPPAAL/DMC – Abstraction-based Heuristics for Directed Model Checking. TACAS 2007. |
| [BDFW07] | Ingo Brückner, Klaus Dräger, Bernd Finkbeiner, and Heike Wehrheim. Slicing Abstractions. FSEN 2007. |
| [DFP06] | Klaus Dräger, Bernd Finkbeiner, and Andreas Podelski. Directed Model Checking with Distance-preserving Abstractions. SPIN 2006. |