Abstract

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 problem.

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.

BibTeX

@phdthesis{CS10,
  author    = "Christian Sternagel",
  title     = "Automatic Certification of Termination Proofs",
  school    = "University of Innsbruck",
  year      = 2010
}