Tool Interoperability in the Maude Formal Environment

Durán, Francisco; Rocha, Camilo; Álvarez, José María

dc.contributor.author	Durán, Francisco
dc.contributor.author	Rocha, Camilo
dc.contributor.author	Álvarez, José María
dc.date.accessioned	2021-12-03T17:29:14Z
dc.date.available	2021-12-03T17:29:14Z
dc.date.issued	2011
dc.identifier.isbn	9783642229442
dc.identifier.issn	9783642229435
dc.identifier.uri	https://repositorio.escuelaing.edu.co/handle/001/1897
dc.description.abstract	We present the Maude Formal Environment (MFE), an executable formal specification in Maude within which a user can seamlessly interact with the Maude Termination Tool, the Maude Sufficient Completeness Checker, the Church-Rosser Checker, the Coherence Checker, and the Maude Inductive Theorem Prover. We explain the high-level design decisions behind MFE, give a summarized account of its main features, and illustrate with an example the interoperation of the tools available in its current release.	eng
dc.description.abstract	Presentamos Maude Formal Environment (MFE), una especificación formal ejecutable en Maude dentro de la cual un usuario puede interactuar sin problemas con la herramienta de terminación de Maude, el verificador de integridad suficiente de Maude, el verificador de Church-Rosser, el verificador de coherencia y el teorema inductivo de Maude. Tirador de pruebas. Explicamos las decisiones de diseño de alto nivel detrás de MFE, brindamos una descripción resumida de sus características principales e ilustramos con un ejemplo la interoperabilidad de las herramientas disponibles en su versión actual.	ESP
dc.format.extent	7 páginas.	spa
dc.format.mimetype	application/pdf	spa
dc.language.iso	eng	spa
dc.publisher	Springer	spa
dc.relation.ispartofseries	Lecture Notes in Computer Science;6859
dc.rights	© Springer-Verlag Berlin Heidelberg 2011	eng
dc.rights.uri	https://creativecommons.org/licenses/by/4.0/	spa
dc.title	Tool Interoperability in the Maude Formal Environment	eng
dc.type	Capítulo - Parte de Libro	spa
dc.type.version	info:eu-repo/semantics/publishedVersion	spa
oaire.accessrights	http://purl.org/coar/access_right/c_14cb	spa
oaire.version	http://purl.org/coar/version/c_970fb48d4fbd8a85	spa
dc.contributor.researchgroup	Informática	spa
dc.publisher.place	Berlín	spa
dc.relation.citationendpage	406	spa
dc.relation.citationstartpage	400	spa
dc.relation.indexed	N/A	spa
dc.relation.ispartofbook	Algebra and Coalgebra in Computer Science	eng
dc.relation.references	Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Bevilacqua, V., Talcott, C.: All About Maude - A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007)	spa
dc.relation.references	Clavel, M., Durán, F., Eker, S., Meseguer, J., Stehr, M.O.: Maude as a formal meta-tool. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1684–1703. Springer, Heidelberg (1999)	spa
dc.relation.references	Clavel, M., Durán, F., Hendrix, J., Lucas, S., Meseguer, J., Ölveczky, P.: The Maude formal tool environment. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol. 4624, pp. 173–178. Springer, Heidelberg (2007)	spa
dc.relation.references	Clavel, M., Palomino, M., Riesco, A.: Introducing the ITP tool: a tutorial. Journal of Universal Computer Science 12(11), 1618–1650 (2006)	spa
dc.relation.references	Durán, F., Lucas, S., Meseguer, J.: MTT: The Maude termination tool (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 313–319. Springer, Heidelberg (2008)	spa
dc.relation.references	Durán, F., Meseguer, J.: Maude’s module algebra. Science of Computer Programming 66(2), 125–153 (2007)	spa
dc.relation.references	Durán, F., Meseguer, J.: A church-rosser checker tool for conditional order-sorted equational maude specifications. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 69–85. Springer, Heidelberg (2010)	spa
dc.relation.references	Durán, F., Meseguer, J.: A maude coherence checker tool for conditional order-sorted rewrite theories. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 86–103. Springer, Heidelberg (2010)	spa
dc.relation.references	Durán, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. Journal of Logic and Algebraic Programming Journal of Logic and Algebraic Programming (2011) (accepted for publication)	spa
dc.relation.references	Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: Gaducci, F., Montanari, U. (eds.) Proceedings of 4th International Workshop on Rewriting Logic and its Applications (WRLA 2002). Electronic Notes in Theoretical Computer Science, vol. 71 (2002)	spa
dc.relation.references	Hendrix, J.: Decision Procedures for Equationally Based Reasoning. Ph.D. thesis. University of Illinois at Urbana-Champaign (2008)	spa
dc.relation.references	Rocha, C., Meseguer, J.: Constructors, sufficient completeness and deadlock freedom of rewrite theories. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 594–609. Springer, Heidelberg (2010)	spa
dc.relation.references	Rocha, C., Meseguer, J.: Proving safety properties of rewrite theories. Tech. rep. University of Illinois at Urbana-Champaign (2010), http://hdl.handle.net/2142/17407	spa
dc.rights.accessrights	info:eu-repo/semantics/closedAccess	spa
dc.rights.creativecommons	Atribución 4.0 Internacional (CC BY 4.0)	spa
dc.subject.armarc	Maude	ENG
dc.subject.armarc	Par crítico	ESP
dc.subject.armarc	Obligación de prueba	ESP
dc.subject.armarc	Parte Funcional	ESP
dc.subject.armarc	Herramienta activa	ESP
dc.subject.armarc	Objetivo de terminación	ESP
dc.subject.proposal	Critical Pair	eng
dc.subject.proposal	Proof Obligation	eng
dc.subject.proposal	Functional Part	eng
dc.subject.proposal	Active Tool	eng
dc.subject.proposal	Termination Goal	eng
dc.type.coar	http://purl.org/coar/resource_type/c_3248	spa
dc.type.content	Text	spa
dc.type.driver	info:eu-repo/semantics/bookPart	spa
dc.type.redcol	http://purl.org/redcol/resource_type/ART	spa