Proving Termination Properties with MU-TERM

Authors

Beatriz Alarcón, Raúl Gutiérrez, Salvador Lucas, and Rafael Navarro-Marset.

Abstract

MU-TERM is a tool which can be used to verify a number of termination properties of (variants of) Term Rewriting Systems (TRSs): termination of rewriting, termination of innermost rewriting, termination of order-sorted rewriting, termination of context-sensitive rewriting, termination of innermost context-sensitive rewriting and termination of rewriting modulo specific axioms. Such termination properties are essential to prove termination of programs in sophisticated rewriting-based programming languages. Specific methods have been developed and implemented in MU-TERM in order to efficiently deal with most of them. In this paper, we report on these new features of the tool.

Publication

In Michael Johnson and Dusko Pavlovic, editors,
Proc. of the 13th International Conference on Algebraic Methodology And Software Technology, AMAST'10,
LNCS 6486:201-208, Springer-Verlag, Berlin, 2011.