Certifying termination and complexity proofs of programs

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. Although undecidable in general, much work has been spent on automated termination and complexity analysis. Whereas the answer to the question for a given program might be simple (yes, the program is terminating), the underlying proof is usually not that simple. In fact, most tools for automated complexity and termination analysis are complex tools, which combine several techniques while trying to analyze the behavior of a program. Consequently, these tools 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. Note that with the help of the certifiers, several bugs have been spotted, both in the implementations of the tools, as well as in soundness proofs of termination techniques. 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 computational model that underlies much of declarative programming and automated theorem proving. 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 extend the work of Klein and Nipkow on Jinja towards Java, and we will develop a formalized semantic for Haskell. 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.

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 analyser-program which decides for each other program, whether it terminates or not. Nevertheless, much work has been spent on the development of such analysers which are often able to guarantee the property of concern. Whereas the answer of 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 simple. In fact, most analysers for the properties complexity and termination are complex programs on their own, which combine several techniques while trying to determine the behaviour of a program. Consequently, these analysers may contain errors and give wrong answers and proofs. Our solution to this problem is the program CeTA (Certified Tool Assertions), a certifier that was developed in this project. CeTA can figure out whether the proofs that are generated by the analysers are correct or not. To make CeTA trustworthy, we formally verified all algorithms within CeTA with the help of the theorem prover Isabelle. In comparison to previous certifiers, CeTA offers the following unique features: - CeTA supports several kinds of complexity proofs from various analysers. - CeTA supports checking termination proofs for LLVM, a widely used intermediate language that is utilised when compiling programs written in popular programming languages such as C and Haskell. - For checking complexity proofs, internally CeTA supports precise calculations via algebraic numbers. For instance, CeTA is able to compute all roots of a polynomial such as x^8 - 5x^6 + 7x^3 - 17 without any rounding errors. - For checking LLVM proofs, CeTA provides a validity checker for linear inequalities, e.g., it can decide whether there are integers x, y and z such that 2x + 3y - 2z > 7, x - 5y + 4z > -2 and 3x + 4y + z < 15. As further results of this project, mistakes in textbooks and published research articles have been spotted (and corrected) during the formalisation of the algorithms that are used in CeTA; wrong proofs of some analysis tools have been identified by CeTA and the corresponding tools have been fixed; and finally, the developed verified algorithms can serve as a good starting point for other formalisations in the area of program analysis.