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.

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"
}