### Finding and Certifying Loops

Harald Zankl, Christian Sternagel, Dieter Hofbauer, and Aart MiddeldorpProceedings of the 36th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2010), Lecture Notes in Computer Science 5901, pp. 755 – 766, 2010.

### 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

@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 }