cl-banner

Finding and Certifying Loops

Harald Zankl, Christian Sternagel, Dieter Hofbauer, and Aart Middeldorp

Proceedings 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.

 

  PDF |    doi:10.1007/978-3-642-11266-9_63  |  © Springer

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
}
Nach oben scrollen