TY - JOUR
T1 - Web Services and Interoperability for the Maude Termination Tool
AU - Durán, Francisco
AU - Lucas, Salvador
AU - Meseguer, José
AU - Gutiérrez, Francisco
N1 - Funding Information:
1 Partially supported by the EU (FEDER) and Spanish MEC under grants TIN 2005-09405-C02-01 and TIN 2008-03107. 2 Partially supported by the EU (FEDER) and Spanish MEC under grant TIN 2007-68093-C02-02. 3 Partially supported by ONR grant N00014-02-1-0715 and NSF Grant CCR-0234524. 4 Email: duran@lcc.uma.es 5 Email: slucas@dsic.upv.es 6 Email: meseguer@cs.uiuc.edu 7 Email: pacog@lcc.uma.es
PY - 2009/8/5
Y1 - 2009/8/5
N2 - 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.
AB - 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.
KW - Maude
KW - rewriting logic
KW - termination
UR - http://www.scopus.com/inward/record.url?scp=68049143137&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=68049143137&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2009.07.061
DO - 10.1016/j.entcs.2009.07.061
M3 - Article
AN - SCOPUS:68049143137
SN - 1571-0661
VL - 248
SP - 83
EP - 92
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
ER -