A.: Finding and certifying loops

Abstract. The first part of this paper presents a new approach for au-tomatically proving nontermination of string rewrite systems. We encode rewrite sequences as propositional formulas such that a loop can be ex-tracted from a satisfying assignment. Alternatively, loops can be found by enumerating forward closures. In the second part we give a formal-ization 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