Theoretical Computer Science
Computer science is a theoretical science. It
„deals with man-made objects. We must first conceive or edify what we then want to examine. We need to develop the intellectual tools with which we can not only explore what is, but also study what is possible.“ (Juris Hartmanis)
But what can we construct? Does what we have constructed also behave as we expect? Computers change our lives.
Do they enrich it too? Do we know what man-made artifacts do, what they can do, and what their limits are?
These questions touch on the fundamentals of computer science. Answering them is difficult and requires the use of sophisticated tools from mathematics. Often the problems cannot be mastered with the available tools and new mathematics has to be developed and adapted for the treatment of computer science problems.
From this broad spectrum of problems, two groups of problems are primarily dealt with in the theoretical computer science department:
Formal Methods in Programming
This problem area deals with the design of systematic methods for the synthesis, verification and optimization of algorithms and software systems. A special focus is on methods that can be described in logical calculi and thus implemented with the help of interactive and automatic proof systems, and on the application of such methods in the development of reliable and efficient software.
Proof calculi for expressive logics are in principle able to formalize and specify every proof problem. However, a practical problem in reasoning is the size of the resulting evidence. While interactive proof systems are a very good tool for constructing formal proofs without errors, the effort involved in finding such proofs makes interactive proof construction impractical for complex proof objectives. Fully automatic proof procedures, on the other hand, are currently only available for relatively weakly expressive logics. The aim of our work is therefore the development of automatic proof procedures for more expressive logics which are suitable for controlling the construction of proofs in interactive proof systems.