Research

Research Topics of the Group

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

The problems which arise in deductive verification, but also in other fields (such as mathematics, databases and cryptography) often involve reasoning in combinations of theories. A large part of our research is therefore devoted to finding methods for efficient reasoning in complex theories.

 

Modeling and verification of complex systems.

For verifying complex systems, we modularly reduce the verification tasks for the full complex systems to simpler verification tasks for their component parts, taking interaction into account. For the verification of the individual systems we use e.g. deductive verification techniques or techniques based on abstraction/refinement.

 

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:

  • knowledge representation (e.g. description logics
  • efficient reasoning in mathematics
  • the verification of cryptographic protocols.