You are here: Home Team Matthias Heizmann

Matthias Heizmann


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 Ultimate Automizer, which is one toolchain of  the Ultimate Program Analysis Framework.




Student Projects

If I find enough time, I love to supervise projects and theses for bachelor and master students. Topics are usually related to my research (program analysis, automata theory) and consist of a rather theoretical part and an implementation of the results in the Ultimate Program Analysis Framework. There is no list that lists all available topics in detail. Usually we sit down with interested students and work out details of the topic together. You can find a list of some available topics in the wiki of Ultimate. For inspiration you may also want to have a look at the projects in progress or the finished projects, often we find some ideas for a related or follow-up project or thesis. It is not mandatory but helpful that you participated in lectures/seminars on program analysis, automata theory, or logic.


You can find an updated list at DBLP and Google Scholar, below is a selection of older papers.


Talks and Posters (to be updated...)