Research

One of the central goals of the research work in the theoretical computer science group is to bring theoretical and practical aspects of computer science together. Two topics are currently in the foreground.

The aim of this research is the design and implementation of formal-logical procedures for the development of reliable software, in particular reliable and efficient distributed systems. The main focus is on the application of logical and automatic proof procedures in program synthesis, verification and optimization.

One of the main applications in recent years has been the development of a logical programming environment for the ENSEMBLE communication system. In collaboration with researchers from Cornell University , we have developed methods that embed the entire code of ENSEMBLE into the logic of the NUPRL evidence system, check the safety-critical properties of ENSEMBLE within NUPRL, and significantly increase the efficiency of ENSEMBLE through the use of knowledge-based optimization techniques (i.e. by the factor 3-5) and thereby generate a proof of the correctness of the optimization.

The aim of this research is the development of fully automated logical proof procedures and their integration into interactive proof systems such as NUPRL, MetaPRL, Coq, Isabelle or PVS. These methods are used to control conceptually simple, but technically complex parts of verifications and syntheses, which considerably simplifies practical work with the program development system.

The research of the last few years has concentrated primarily on evidence-seeking procedures based on matrix characterizations of logical validity. Matrix characterizations enable a very compact representation of the search space as well as the extraction of evidence objects to control interactive evidence systems. For constructive, modal and linear logics we have developed a uniform proof procedure and implemented a prover JPROVER to control proofs in NUPRL. JPROVER is now also used in MetaPRL and Coq.

In the coming years we want to increase the efficiency of these procedures considerably through the integration of induction techniques, decision procedures, evidence planners, and mathematical knowledge bases and test them in practical applications.