Short: software verification. More detailed: I am working on automatic methods that verify safety and liveness properties of sequential and concurrent programs. My research interests include also automata theory, formal language theory, synthesis of termination arguments and interpolant generation.
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.
Parts of my research are implemented in the ULTIMATE Program Analysis Framework.
- Ultimate Automizer with SMTInterpol, in TACAS 2013, together with Jürgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke, Markus Lindenmann, Alexander Nutz, Christian Schilling, and Andreas Podelski. [bib]
- pdf ] , in , together with Neil D. Jones and Andreas Podelski. [ |
- pdf] , in , together with Jochen Hoenicke and Andreas Podelski. [ |
[ | ] , in , together with Jochen Hoenicke and Andreas Podelski.
Slides of Talks
- Trace Abstraction, November 2010, at .
- Nested Interpolants, January 2010, at .
- , August 2009, at , presented by Jochen Hoenicke.
- Trace Abstraction, March 2009, at 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 talk.
I suggest to have a look at the slides of the SAS09 talk which is an improved and extended version based on this talk. , Oktober 2008, at Software Analysis Workshop in Alacati.
- Abstract Interpretation Seminar in Winter Term 07/08, about (which was published by Patrick Cousot, Pierre Ganty and Jean-François Raskin in SAS 2007) at the
- at the in Summer Term 2007, about (which was published by Patrick Cousot & Radhia Cousot in Pacific Journal of Mathematics, Vol. 82)
Available Student Projects
- Minimization of Nested Word Automata
- Complementation of Büchi Automata
- Predicates and Prejudice - Proving Correctness of Programs
- Verification of Concurrent Programs
If you are interested in a different topic feel free to ask me. If you find some of the already finished student projects interesting, feel free to ask for a follow up project.
- Seminar: Automata Theory (Summer Term 2013)
- Master Thesis: Nested Word Automata Minimization (reserved)
- Bachelor Thesis: Formula Simplification (starting soon)
- Master Thesis: LTL Software Model Checking (in progress)
- Master Thesis: Synthesis of Ranking Functions (in progress)
- Master Team Project: Minimal Unfolded Petri Nets (in progress)
- Master Team Project: Rank-based Büchi Nested Word Automata Complementation (in progress)
- Bachelor Project: User Interface for Automata Library (in progress)
- Master Team Project: Synthesis of Ranking Functions for Lasso Programs
- Master Laboratory: Implementation of Rank-based Büchi Automata Complementation
- Master Laboratory: Implementation of a Nested Word Automata Minimization
- Bachelor Thesis: Trace Abstraction for Concurrent Programs via Petri Net Acceptors
- Seminar: Automata Theory (Summer Term 2012)
- Master Team Project: Ultimate Team Project
- Master Laboratory: Implementation of Ranking Function Synthesis
- Master Laboratory: Reducing the Size of Büchi Automata
- Lecture Program Verification (Winter Term 11/12)
- Seminar Static Checkers for Java and C# (Summer Term 2011)
- Bachelor Project: Implementation of On-line Formula Simplification
- Bachelor Project: Implementation of a Petri Net Unfolder
- Master Thesis: Three Operations on Büchi Nested Word Automata for Program Verification
- Lecture Theory2 (Winter Term 10/11)
- Lecture Informatik III - Theoretische Informatik (Winter Term 10/11)
- Bachelor Thesis: Petri Net Acceptors
- Master Thesis: Implementation of Nested Interpolants
- Seminar: Advanced Topics in Model Checking (Summmer Term 2010)
- Master Team Project: Büchi Nested Word Automata
- Master Laboratory: A Study of Software Model Checkers based on Interpolation
- Bachelor Thesis: Complexity of Intersection Emptiness of Visibly Pushdown Languages
- Lecture: Informatik III - Theoretische Informatik (Winter Term 09/10)
- Bachelor Project: Nested Word Automata
- 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 (Summer Term 2007)
- Tutorial for lecture (Winter Term 06/07)