Mission Statement

We are concerned with the logical foundations of computer science and their application to the analysis and verification of complex systems. The two main themes are:

Verification and Formalization: We aim to provide the highest certainty about computer programs as well as mathematical proofs. To this end, we develop a large formal library of properties stemming from various domains including term rewriting, programming languages, and linear algebra. We also develop proof advice tools that automate reasoning by combining automatic deduction with machine learning.

Term Rewriting and Resource Analysis: We aim to study programs in a general setting. On the one hand we continue our internationally leading research on rewrite systems, in particular we are constantly expanding our award-winning suite of rewrite tools. On the other hand we are developing highly competitive tools for the static resource analysis of programs.