Improving Certifiers for Termination Proofs

Termination (all computation paths produce a result) is a fundamental property of programs. Although undecidable in general, much work has been spent on automated termination analysis. In this proposal, we focus on termination analysis of term rewriting, a simple yet powerful computational model that underlies much of declarative programming and automated theorem proving. Our motivation is that termination analysis of programs in other programming languages can often be done via term rewriting. For example, there are transformations from Prolog, Haskell, and Java into term rewrite systems, such that termination of the resulting rewrite system ensures termination of the original program. In the recent past, there has been a lot of progress in establishing sufficient and automatable criteria for termination of term rewrite systems. Furthermore, those criteria have been incorporated into automated tools. Most of these tools use the dependency pair framework, which allows a modular combination of termination techniques. In this framework, termination proofs are represented by proof trees where at each node some termination technique is applied. Note that current tools automatically find proof trees, which reach sizes up to several megabytes. Since every now and then faulty proofs have been generated by termination tools - where even termination proofs for nonterminating systems have been generated - it has been identified as a key challenge to independently certify the correctness of the obtained proofs. Due to the size of these proofs a manual inspection is infeasible and also error-prone. However, it can be done using interactive theorem provers like Coq, Isabelle, or PVS. These theorem provers are used to model various aspects of mathematics, programming languages, etc. in a logical system and afterwards formally verify desired properties. Certifying termination proofs is usually done in two stages: First, formally prove soundness of several termination techniques, using the theorem prover. Second, certify that each node of a proof tree resembles a correct application of some termination technique. For example, in the first stage it is proven once and for all that lexicographic path orders are reduction orders. And in the second stage it is checked for a concrete precedence and a concrete rewrite system that all rules are oriented by the corresponding lexicographic path order. Hence, we may detect faulty theorems or reveal implementation bugs in termination tools. At the moment there are three independent certifiers. Our certifier, IsaFoR/CeTA (available at http://cl- informatik.uibk.ac.at/software/ceta/) is based on Isabelle/HOL. All certifiers use the described two-stage approach to certify termination proofs. As input they expect a termination proof in a common proof format and then accept or reject that proof. With their help, both bugs in theorems of published papers and bugs in termination tools have been detected and could be fixed. The main aim of this project is to increase the applicability of our certifier IsaFoR/CeTA, which consists of an Isabelle/HOL-library on rewriting (IsaFoR) and an extracted binary certifier (CeTA). We aim for the following four goals: A) Support more termination techniques to increase the number of certifiable proofs. B) Closely couple termination tools with CeTA such that large parts of each proof can be certified, even if the proof contains termination techniques that have not been formalized. C) Prove termination of Isabelle/HOL-functions by importing proofs from termination tools via IsaFoR. This will increase the degree of automation in the interactive prover Isabelle/HOL. D) Certify implicit complexity bounds of termination proofs such that safe runtime bounds can be ensured, in addition to the certified property of termination.

For computer software which is utilized in safety critical domains (like aviation, fire alarms, medical equipment), it is of major importance that it works reliable. To this end, in this project we considered two crucial properties of programs: a program is terminating if it always returns a result and does not compute forever; and the complexity describes how long we have to wait for the result. For both properties there are analyzers available which automatically determine the complexity and the termination behavior for many programs.The major risk is that the analyzers themselves are programs which might contain errors and thus deliver wrong answers, e.g., claim termination of a non-terminating program. To minimize this risk, one can demand that the analyzers also produce certificates in addition to their answers, which contain the reasoning why the answers are correct. These certificates can then automatically be checked by some trusted certifier, where the reliability of the certifier is guaranteed by some complex formal correctness proof.Note that certification is only possible if all the applied termination and complexity techniques in the certificates are supported by the certifier, which often limits the applicability. To change this situation, in this project we formally proved correctness of several termination and complexity techniques within the proof assistant Isabelle and integrated them into our certifier. Since many termination techniques rely on confluence (all computations lead to the same result), as a side product, our certifier can now also be combined with confluence analyzers. Furthermore, we also integrated support for partial certificates, so that we can even check certificates that contain unsupported reasons. In that case, the typical answer of the certifier is that 90 % of the reasoning in the certificate could be validated.As a result of the increased applicability of the certifier, we could detect and fix several errors in state-of-the-art analyzers which remained undetected for years. This includes both implementation bugs in the analyzers as well as mistakes in published research articles, which unfortunately often only provide informal correctness proofs.