Finding and Certifying Loops

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. Key words: Rewriting, Nontermination, Certification

• Type: Conference
• Year: 2010
• Where: SOFSEM
• Authors: Harald Zankl, Christian Sternagel, Dieter Hofbauer, Aart Middeldorp
• Keywords: Rewrite Sequences, SOFSEM 2010, Theorem Prover Isabelle/hol, Theoretical Computer Science, first Tool