Skip to content
Technical University of Munich

Software underpins every area of modern society. Automated reasoning about programs is essential for their correctness, safety, and trustworthiness, and is becoming increasingly important as AI systems generate an increasing share of software. We investigate the mathematical foundations of programs, programming languages, and computational systems and develop models, logics, algorithms, and tools that enable their properties to be analysed and verified automatically.

Research

Our research comprises four closely connected areas:

  • Foundations of programs and programming languages: precise mathematical models, formal semantics, type systems, and concepts such as ownership and borrowing; a current focus is the Rust programming language
  • Program analysis and software verification: static analysis, automated analysis of termination, resource consumption, and complexity, as well as separation logic and shape analysis for memory-safety verification
  • Logic, automata, and infinite-state systems: the expressiveness, decidability, and complexity of logics, automata, and related mathematical models, including vector addition systems (Petri nets) and graph grammars
  • Formal methods and artificial intelligence: using machine learning to support automated reasoning and logical methods to understand AI models; current topics include machine-learned guidance for proof search and logical characterisations of neural networks
Teaching

Our teaching covers the foundations of programming as well as advanced topics in programming languages, program analysis, and formal methods. These include functional programming, compiler construction, program optimisation and verification, as well as logic, automata theory, and automated reasoning.

Information about the courses currently offered can be found under Teaching.

Working with us

We supervise Bachelor’s and Master’s theses in all of these areas and are happy to discuss topics not included in our current list. See topics for theses.

We also welcome enquiries from prospective doctoral researchers with a background in logic and automata theory, programming languages, program analysis, verification, or theoretical machine learning, as well as enquiries about research collaborations.

To top