Abstract

The first part of this paper presents a new approach for automatically proving nontermination of string rewrite systems. We encode rewrite sequences as propositional formulas such that a loop can be extracted from a satisfying assignment. Alternatively, loops can be found by enumerating forward closures.

In the second part we give a formalization of loops in the theorem prover Isabelle/HOL. Afterwards, we use Isabelle's code-generation facilities to certify loops. The integration of our approach in CeTA (a program for automatic certification of termination proofs) makes it the first tool capable of certifying nontermination.

BibTeX Entry

@inproceedings{ZSHM-SOFSEM10,
 author    = "Harald Zankl and Christian Sternagel and Dieter Hofbauer and
              Aart Middeldorp",
 title     = "Finding and Certifying Loops",
 booktitle = "Proceedings of the 36th International Conference on Current
              Trends in Theory and Practice of Computer Science",
 series    = "Lecture Notes in Computer Science",
 volume    = 5901,
 pages     = "755--766"
 year      = 2010,
 doi       = "10.1007/978-3-642-11266-9\_63"
}