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
}