June 16, 2014: CL member René Thiemann is entering the START program

Last Friday Thiemann could convince the international START-/Wittgenstein-Jury of his project “Certifying Termination and Complexity Proofs of Programs”. As a result, his 6-year project is now sponsored by the FWF by more than 1,000,000 EUR.

About the project:

Computer programs become ubiquitous in our world: they are used to manage our money, to control activities in vehicles, and to interact with medical equipment. Therefore, it is of vital importance that programs behave correctly. Here, termination (all computations produce a result) and complexity (how long does it take to get the result, and how much memory is required) are fundamental properties of programs. Unfortunately, these fundamental properties are undecidable. For example, it is not possible to design an analyzer-program which decides for each other program, whether it terminates or not. Nevertheless, much work has been spent on the development of such analyzers which are often (but not always) able to guarantee the property of concern.
Whereas the answer to an analysis for a given program might be simple (yes, the program is terminating), the underlying argument for this answer, i.e., the proof, is usually not that simple. In fact, most analyzers for complexity and termination are complex programs, which combine several techniques while trying to analyze the behavior of a program. Consequently, these analyzers may contain errors and give wrong answers and proofs.
One solution to this problem is the usage of certifiers, which can check the proofs that are generated by the tools. For reliability, the soundness of the certifiers itself has to be formally proven within a theorem prover. This is a challenging and time-consuming task, but it is also rewarding: With the help of the certifiers, several bugs have been spotted, both in the implementations of the analyzers, as well as in soundness proofs of termination techniques which are utilized by the analyzers. Unfortunately, so far the applicability of the available certifiers in this area is rather limited: they mainly handle termination proofs, but not complexity proofs; and they are limited to term rewriting, a simple programming language which can be seen as the foundation of functional programming languages, but which is more of theoretical interest due to its simplicity.
In this project, we will extend the applicability of certifiers in two important directions: we want to support a large class of complexity proofs, and we want to support termination proofs for two real programming languages, Java and Haskell. To this end, we will develop several interesting formalizations. This includes a large library on linear algebra, which will be required for dealing with complexity proofs. Moreover, we will develop a formalized semantics for Haskell and we will extent the existing formalization on Jinja towards Java. (Jinja is a restricted version of Java where certain language constructs are missing.) Our work will drastically improve the reliability of current termination and complexity tools. Furthermore, it can serve as a starting point for performing other formalizations in the area of program analysis and program transformations.