Abstract

This paper describes the second edition of the Tyrolean Termination Tool—a fully automatic termination analyzer for first-order term rewrite systems. The main features of this tool are its (non-)termination proving power, its speed, its flexibility due to a strategy language, and the fact that the source code of the whole project is freely available. The clean design together with a stand-alone OCaml library for term rewriting, make it a perfect starting point for other tools concerned with rewriting as well as experimental implementations of new termination methods.

BibTeX Entry

@inproceedings{KSZM-RTA09,
 author    = "Martin Korp and Christian Sternagel and Harald Zankl and
              Aart Middeldorp",
 title     = "Tyrolean {T}ermination {T}ool 2",
 booktitle = "Proceedings of the 20th International Conference on Rewriting
              Techniques and Applications",
 series    = "Lecture Notes in Computer Science",
 volume    = 5595,
 pages     = "295--304",
 year      = 2009,
 doi       = "10.1007/978-3-642-02348-4\_21"
}