Certification of Nontermination Proofs

Christian Sternagel and René Thiemann

Proceedings of the 3rd International Conference on Interactive Theorem Proving (ITP 2012), Lecture Notes in Computer Science 7406, pp. 266 – 282, 2012.


Automatic tools for proving (non)termination of term rewrite systems, if successful, deliver proofs as justification. In this work, we focus on how to certify nontermination proofs. Besides some techniques that allow to reduce the number of rules, the main way of showing nontermination is to find a loop, a finite derivation of a special shape that implies nontermination. For standard termination, certifying loops is easy. However, it is not at all trivial to certify whether a given loop also implies innermost nontermination. To this end, a complex decision procedure has been developed in earlier work. We formalized this decision procedure in Isabelle/HOL and were able to simplify some parts considerably. Furthermore, from our formalized proofs it is easy to obtain a low complexity bound. Along the way of presenting our formalization, we report on generally applicable ideas that allow to reduce the formalization effort and improve the efficiency of our certifier.


  PDF |    doi:10.1007/978-3-642-32347-8_18  |  © Springer


author = "Christian Sternagel and Ren{\'e} Thiemann",
title = "Certification of Nontermination Proofs",
booktitle = "Proceedings of the 3rd International Conference on Interactive Theorem Proving",
series = "Lecture Notes in Computer Science",
volume = 7406,
pages = "266--282",
publisher = "Springer-Verlag",
year = 2012
Nach oben scrollen