Formal Methods and theoretical Computer Science

Head of the Formal Methods and theoretical Computer Science Research Group

The research focus of the ``Formal Methods and Theoretical Computer Science'' group is the development of provably correct procedures for the verification and analysis of complex systems.

The goal of our research is to identify frameworks under which efficient automatic verification procedures for complex systems exist. In doing so, we investigate possibilities to exploit modularity in verification on different levels, e.g.: Possibilities for efficient modular reasoning in complex logical theories, and modeling and modular verification of complex systems in general.

Our theoretical contributions form the basis for the development of practically applicable tools for the verification of safety-critical systems, in particular in the context of the SFB Transregio project AVACS (Automatic Verification and Analysis of Complex Systems). We use our methods both in program verification and to verify various control systems (e.g., radio controllers for train systems, or hybrid control systems for chemical plants). We also apply our approaches in cryptography, databases, or mathematics.

Research

Our research focuses on the modular verification of complex systems; of particular interest is modular reasoning in complex theories. We analyze various application areas.

Reasoning in complex theories

Modeling and verification of complex systems

Applications