cl-banner

Certification of Nontermination Proofs using Strategies and Nonlooping Derivations

Julian Nagele, René Thiemann, and Sarah Winkler

Proceedings of the 6th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2014), Lecture Notes in Computer Science 8471, pp. 216 – 232, 2014.

Abstract

The development of sophisticated termination criteria for term rewrite systems has led to powerful and complex tools that produce (non)termination proofs automatically. While many techniques to establish termination have already been formalized-thereby allowing to certify such proofs-this is not the case for nontermination. In particular, the proof checker was so far limited to (innermost) loops. In this paper we present an Isabelle/HOL formalization of an extended repertoire of nontermination techniques. First, we formalized techniques for nonlooping nontermination. Second, the available strategies include (an extended version of) forbidden patterns, which cover in particular outermost and context-sensitive rewriting. Finally, a mechanism to support partial nontermination proofs further extends the applicability of our proof checker.

 

  PDF |    doi:10.1007/978-3-319-12154-3_14  |  © Springer International Publishing Switzerland 2014

BibTeX 

@inproceedings{JNRTSW-VSTTE14,
author = "Julian Nagele and René Thiemann and Sarah Winkler",
title = "Certification of Nontermination Proofs using Strategies and Nonlooping Derivations",
booktitle = "Proceedings of the 6th International Conference on Verified
Software: Theories, Tools, and Experiments",
editor = "Dimitra Giannakopoulou and Daniel Kroening ",
series = "Lecture Notes in Computer Science",
volume = 8471,
pages = "216--232",
year = 2014,
doi = "10.1007/978-3-319-12154-3_14"
}
Nach oben scrollen