Research

Our research can be roughly subsumed under the wide field of Formal Methods for the construction and analysis of systems.

Topics of interest are: tools for compiler construction, static analysis by abstract interpretation and model checking, efficient generic fixpoint algorithms, expressive domains for numerical invariants, analyses of concurrent systems, precision of analyses, analysis of safety critical C programs, information flow analysis, analysis of cryptographic protocols, tree automata and Horn clauses, tree transducers and XML processing, equivalence problems for tree transducers.

We are also interested in innovative technical systems for teaching and the visualization of systems behavior.

Most of our ideas have been realized in prototypical systems such as CUP (a frontend generator for Java), Goblint (an analyzer for multithreaded C) or ttt (a tool for lecture recording).

Our research group has been making contribution to the construction of quantum computers within Munich Quantum Valley. Have a look at Yanbin Chen for further interest. Currently we mainly focus on static analysis and optimizations for dynamic quantum circuits.