LEO II
Aim of the LEO II project is to build a state-of-the-art theorem prover for higher order logic, incorporating the lessons of recent research. Currently we figure out how to implement a kit of efficient data structures for higher order theorem proving.

Verisoft XT
Verisoft XT is a three-year research project funded by the German Federal Ministry of Education and Research (BMBF). Project management agency is the German Aerospace Center (DLR). The main goal of the project is the pervasive formal verification of computer systems. The correct functionality of systems, as they are used, for example, in automotive engineering, in security technology and in the sector of medical technology, is to be mathematically proved.

SigmaKEE
The Sigma knowledge engineering environment is an system for developing, viewing and debugging theories in first order logic. It works with Knowledge Interchange Format (KIF) and is optimized for the Suggested Upper Merged Ontology (SUMO).

OMEGA
The OMEGA system is at the core of several related and well-integrated research projects of the OMEGA research group, whose aim is to develop system support for the working mathematician. My task here is the implementation of a small white-box CAS, i.e., a CAS whose computation can be traced and checked within the Theorem Prover's formalism.