We are concerned with the logical foundations of computer science and their application to the analysis and verification of complex systems.
A major research theme is the study of term rewriting, a formal model of computation that underlies declarative programming and which is heavily used in symbolic computation in mathematics (exemplified by Mathematica) and theorem proving. Besides fundamental research in term rewriting, we are developing the Tyrolean Termination Tool, a very powerful tool for automatically proving termination of rewrite systems. One of the reasons for the success of this tool is the incorporation of modern SAT solving technology, which lately has received much attention in industry.
Another important research theme is verification. Modern engineering applications have reached a level of complexity where the judgement of experts is no longer sufficient to ensure their correctness or safety. This is true, in particular, for software systems. Theorem provers can, in principle, be used to rigorously check the correctness of such systems and we apply this technology to ensure the correctness of mathematical software. On the other hand, in complex software systems computations may arise that require more time and space resources than available. Although the system is correct in theory, it may still not be reliable in practice. Hence we are also concerned with logic-based resource analysis to ensure safety of software systems.
In both strands we develop state-of-the-art logic-based technology to overcome limitations in current system design, implementation and verification.