Web Services and Interoperability for the Maude Termination Tool

Citations of this article
Mendeley users who have this article in their library.


This paper presents the Maude Termination Tool (MTT) version 1.5. MTT takes Maude programs as inputs and tries to prove them terminating by applying different transformation techniques and by using existing termination tools as back-ends. MTT can use as back-end tool any termination tool supporting the TPDB syntax, either locally if it follows the rules for the Termination Competition, or remotely as web services. This allows us to interact with the different tools in a uniform way, and not restricting ourselves to a specific set of tools. Thus, tools that have participated in the competition, like AProVE, MU-TERM, TTT, etc., or others that accommodate to the syntax and form of interaction, can be used as back-ends of MTT. In the MTT environment, Maude specifications can be proved terminating by using (any of these) distinct formal tools, allowing the user to choose the most appropriate one for each particular case, a combination of them, or trying different alternatives in the case of a particular tool cannot find a proof. © 2009 Elsevier B.V. All rights reserved.

Author supplied keywords




Durán, F., Lucas, S., Meseguer, J., & Gutiérrez, F. (2009). Web Services and Interoperability for the Maude Termination Tool. Electronic Notes in Theoretical Computer Science, 248, 83–92. https://doi.org/10.1016/j.entcs.2009.07.061

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free