Automatic Certification of Termination Proofs

Christian Sternagel

PhD thesis, University of Innsbruck, 2010.


Proving the correctness of computer software is of utmost importance for safety-critical systems. A crucial part of proving correctness is to show that a computer program always yields a result. This property, called termination, is undecidable in general. Instead of handling a specific programming language, we use a mathematical model of computation, namely term rewriting.
But how do we prove termination of a given term rewrite system? This has been a topic of research, for several decades. Many so called termination techniques have been developed. Some of them are convenient for proving termination by hand, others are especially suitable for automation. Most of these techniques have been integrated in at least one automated termination tool. Such tools are programs that take a term rewrite system and try to either prove or disprove termination. Furthermore, there are recent and powerful automatic methods for proving termination. Thus, by using a termination tool it is sometimes possible to prove termination of a term rewrite system at the touch of a button.
But how do we know that the termination tool is correct? The short answer is: we do not. Indeed, there have already been some occasions, where a termination tool delivered a wrong proof. This is not too surprising, since the average termination tool is a complex piece of software that has to combine many different termination techniques in an efficient way. Combining many different techniques additionally results in huge proofs: modern termination tools may easily generate proofs reaching sizes of several megabytes. To avoid manual checking and still maintain a high level of confidence in the correctness of the generated proofs, we implement a trustworthy termination proof checker that reads a given termination proof and checks its correctness automatically. The obstacle of developing a trustworthy proof checker is generally tackled by using an interactive theorem prover. In our thesis we use Isabelle/HOL. Our checker is built in two stages:
First, we formalize all the mathematical theory that is used in automated termination tools. Additionally, we formalize functions that check, whether some termination technique is applied correctly. This is done in our Isabelle Formalization of Rewriting. Then, we extract the termination proof checker using Isabelle’s code-generation facilities. Resulting in our Certified Termination Analyser.
As already stated above, the IsaFoR/CeTA project mainly arose out of the need to automatically check termination proofs that are generated by termination tools. Additionally, we wanted to give an Isabelle formalization of term rewriting that can be used as the bases for related projects. In our thesis we describe only parts of IsaFoR/CeTA. More specifically:
We formalize large parts of the basic infrastructure available in IsaFoR. Starting from abstract rewriting, via terms, contexts, positions, substitutions, and so on, up to the dependency pair framework (today’s de facto standard for modular termination proofs).
Moreover, we formalize the dependency pair transformation and the corresponding theorem, stating that the termination of a given term rewrite system is equivalent to finiteness of the resulting dependency pair problems.
Furthermore, we formalize the subterm criterion, a termination technique for the dependency pair framework. This also serves as the basis for a variant of the size-change principle that can be used to prove finiteness of dependency pair problems.
Building on the dependency pair transformation, we give an alternative (and in our opinion elegant) proof of the fact that signature extensions of term rewrite systems preserve termination. Additionally, we first prove and formalize that for (a certain class of) dependency pair problems, signature restrictions reflect (minimal) infinite chains.
Finally, we formalize root-labeling, a transformation on term rewrite systems as well as dependency pair problems, based on semantic labeling. However, in most cases root-labeling can only be applied after another transformation, the so called closure under flat contexts. This is strongly related to signature extensions.




author = "Christian Sternagel",
title = "Automatic Certification of Termination Proofs",
school = "University of Innsbruck",
year = 2010
Nach oben scrollen