Web Services and Interoperability for the Maude Termination Tool

Francisco Durán, Salvador Lucas, José Meseguer, Francisco Gutiérrez

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish (US)
Pages (from-to)83-92
Number of pages10
JournalElectronic Notes in Theoretical Computer Science
StatePublished - Aug 5 2009


  • Maude
  • rewriting logic
  • termination

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Web Services and Interoperability for the Maude Termination Tool'. Together they form a unique fingerprint.

Cite this