Coordinates
building, room
052-00-019
+49 761 203 8235 (phone)
+49 761 203 8242 (fax)
Research
I am working on Verification of Software and Real-Time Systems via model-checking and abstract interpretation.My research interests include also automata theory, formal language theory, satisfiability modulo theories and duration calculus.
I am investigating a verification technique in which a system can be considered as an intersection of languages. In this setting, verification problems can be reduced to well-known descision problems of languages. The crux of the approach is to abstract complex languages by more tractable languages. To refine such an abstraction automatically, I am investigating a technique in which automata are constructed from interpolants that are derived from spurious counterexamples.
My SAS'09 paper, written with Jochen Hoenicke and Andreas Podelski, describes how this technique can be used to verify safety properties of sequential programs. Currently I am investigating how one can extend this technique to recursive programs, concurrent programs, phase event automata and liveness properties. An implementation that uses this techniques, written as a plugin to our model checker Ultimate, will be available soon.
Publications
- Refinement of Trace Abstraction, in SAS 2009, together with Jochen Hoenicke and Andreas Podelski. [ bib | pdf ]
- Nested Interpolants, accepted at POPL 2010 :-), together with Jochen Hoenicke and Andreas Podelski.
Slides of Talks
- Refinement of Trace Abstraction, at August 2009, on SAS 2009, presented by Jochen Hoenicke.
- Trace Abstraction, at March 2009, on R1 meeting of the AVACS Workshop Spring 2009 in Freiburg.
Available on request, but I suggest to have a look at the slides of the SAS09 talk which is an improved and extended version based on this. - Regular Abstraction, at Oktober 2008, on Software Analysis Workshop in Alacati.
I suggest to have a look at the slides of the SAS09 talk which is an improved and extended version based on this. - My Talk at the Abstract Interpretation Seminar in Winter Term 07/08, about Fixpoint-Guided Abstraction Refinements (which was publicated by Patrick Cousot, Pierre Ganty and Jean-François Raskin in SAS 2007)
- My Talk at the Advanced Topics in Model-Checking Seminar in Summer Term 2007, about Constructive Versions of Tarski's Fixed Point Theorems (which was publicated by Patrick Cousot & Radhia Cousot in Pacific Journal of Mathematics, Vol. 82)
Teaching
- Lecture Informatik III - Theoretische Informatik (Winter Term 09/10)
- Seminar Kryptographische Protokolle (Summer Term 2009)
- Tutorial for lecture Formal Techniques for Networked and Distributed Systems (Winter Term 08/09)
- Tutorial for lecture Verification (Winter Term 07/08)
- Tutorial for lecture Softwaretechnik (Summer Term 2007)
- Tutorial for lecture Theoretische Informatik (Winter Term 06/07)