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

In our research we aim at developing general methods, which can be used in a wide variety of application domains:

Verification: We analyzed the applicability of the methods we developed on various examples from the verification of reactive, real-time and hybrid systems (which we analyze in the AVACS project), in particular for increasingly more complex controllers of systems of trains, cars, and for chemical plants.

We also use these methods for: