Abstract

Termination is the important property of a program that all computation paths produce a result in finite time. Although undecidable in general, much work has been spent on automated termination analysis. As a result, today there are a variety of powerful tools for automatic termination analysis. Several of these tools are competing in the annual international termination competition where the aim is to automatically investigate termination and complexity of programs in different languages.


Due to the complexity of the tools itself, it is obvious that there might be bugs in the implementations leading to wrong answers. And indeed, nearly every year in the competition some bugs were spotted since two tools gave contradicting answers, e.g., by providing a termination and a nontermination proof for the same program. Therefore, it has been identified as a key challenge to independently certify the correctness of the generated 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, and 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.


In this thesis, we report on our work in this area, i.e., the development of the certifier CeTA (Certified Termination Analysis) and its underlying formalization IsaFoR (Isabelle Formalization of Rewriting).


With the help of CeTA, several implementation bugs have been revealed which previously remained undetected. All of these problems have been fixed in the meantime, so that the termination tools became more reliable due to certification. In addition to the implementation bugs, during the formalization of the termination techniques in IsaFoR we also discovered some flaws in pen-and-paper proofs which in at least one case invalidated the main theorem of a termination technique.


The amount of our work can be best described in numbers: The size of the formalization IsaFoR is over 100,000 lines. The generated certifier CeTA is a Haskell program of over 24,000 lines. The collection of termination techniques covered by CeTA suffices to certify over 88 % of the termination proofs that are constructed by the currently strongest termination tool for term rewriting.

BibTeX

@misc{RT13,
  author    = "Ren{\'e} Thiemann",
  title     = "A Formalization of Termination Techniques in Isabelle/{HOL}",
  school    = "University of Innsbruck",
  year      = 2013,
  note      = "Habilitation thesis"
}