René Thiemann, computer scientist at the University of Innsbruck received the START-Programme Award, the most prestigious award for young researchers in Austria. René Thiemann’s project deals with the improvement of programs. His aim is to extend the application of Certifiers in regard to reliability and complexity.
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.
Priv.-Doz. Dr. René Thiemann
René Thiemann was born in Stadtlohn (Nordrhein-Westfalen) in 1976. After studing and receiving his PhD at the RWTH Aachen he moved to Innsbruck to work at the Institute of Computer Science at the University of Innsbruck in 2007. Im July 2014 he received his Habilitation for his work „A Formalization of Termination Techniques in Isabelle/HOL“.
START-Programme Award from the Austrian Science Foundation
The START Programme is the most prestigious award directed at young researchers in Austria. For the coming six years the awardees can plan their reserach activities in a sound financial environment which enables them to establish their own reserach groups. A total of 8 START-Programme Awards were awarded in Austria this year – three of them go to researchers at the University of Innsbruck – the Mathematician Karin Schnass and the Micro Biologist Sigrid Neuhauser.