Tool Interoperability in the Maude Formal Environment
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....
- Autores:
-
Durán, Francisco
Rocha, Camilo
Álvarez, José María
- Tipo de recurso:
- Part of book
- Fecha de publicación:
- 2011
- Institución:
- Escuela Colombiana de Ingeniería Julio Garavito
- Repositorio:
- Repositorio Institucional ECI
- Idioma:
- eng
- OAI Identifier:
- oai:repositorio.escuelaing.edu.co:001/1897
- Acceso en línea:
- https://repositorio.escuelaing.edu.co/handle/001/1897
- Palabra clave:
- Maude
Par crítico
Obligación de prueba
Parte Funcional
Herramienta activa
Objetivo de terminación
Critical Pair
Proof Obligation
Functional Part
Active Tool
Termination Goal
- Rights
- closedAccess
- License
- © Springer-Verlag Berlin Heidelberg 2011
| id |
ESCUELAIG2_bdaad4dbc54081ad543aab69c00f3f12 |
|---|---|
| oai_identifier_str |
oai:repositorio.escuelaing.edu.co:001/1897 |
| network_acronym_str |
ESCUELAIG2 |
| network_name_str |
Repositorio Institucional ECI |
| repository_id_str |
|
| dc.title.eng.fl_str_mv |
Tool Interoperability in the Maude Formal Environment |
| title |
Tool Interoperability in the Maude Formal Environment |
| spellingShingle |
Tool Interoperability in the Maude Formal Environment Maude Par crítico Obligación de prueba Parte Funcional Herramienta activa Objetivo de terminación Critical Pair Proof Obligation Functional Part Active Tool Termination Goal |
| title_short |
Tool Interoperability in the Maude Formal Environment |
| title_full |
Tool Interoperability in the Maude Formal Environment |
| title_fullStr |
Tool Interoperability in the Maude Formal Environment |
| title_full_unstemmed |
Tool Interoperability in the Maude Formal Environment |
| title_sort |
Tool Interoperability in the Maude Formal Environment |
| dc.creator.fl_str_mv |
Durán, Francisco Rocha, Camilo Álvarez, José María |
| dc.contributor.author.none.fl_str_mv |
Durán, Francisco Rocha, Camilo Álvarez, José María |
| dc.contributor.researchgroup.spa.fl_str_mv |
Informática |
| dc.subject.armarc.ENG.fl_str_mv |
Maude |
| topic |
Maude Par crítico Obligación de prueba Parte Funcional Herramienta activa Objetivo de terminación Critical Pair Proof Obligation Functional Part Active Tool Termination Goal |
| dc.subject.armarc.ESP.fl_str_mv |
Par crítico Obligación de prueba Parte Funcional Herramienta activa Objetivo de terminación |
| dc.subject.proposal.eng.fl_str_mv |
Critical Pair Proof Obligation Functional Part Active Tool Termination Goal |
| description |
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. |
| publishDate |
2011 |
| dc.date.issued.none.fl_str_mv |
2011 |
| dc.date.accessioned.none.fl_str_mv |
2021-12-03T17:29:14Z |
| dc.date.available.none.fl_str_mv |
2021-12-03T17:29:14Z |
| dc.type.spa.fl_str_mv |
Capítulo - Parte de Libro |
| dc.type.coar.fl_str_mv |
http://purl.org/coar/resource_type/c_2df8fbb1 |
| dc.type.coarversion.fl_str_mv |
http://purl.org/coar/version/c_970fb48d4fbd8a85 |
| dc.type.version.spa.fl_str_mv |
info:eu-repo/semantics/publishedVersion |
| dc.type.coar.spa.fl_str_mv |
http://purl.org/coar/resource_type/c_3248 |
| dc.type.content.spa.fl_str_mv |
Text |
| dc.type.driver.spa.fl_str_mv |
info:eu-repo/semantics/bookPart |
| dc.type.redcol.spa.fl_str_mv |
http://purl.org/redcol/resource_type/ART |
| format |
http://purl.org/coar/resource_type/c_3248 |
| status_str |
publishedVersion |
| dc.identifier.isbn.none.fl_str_mv |
9783642229442 |
| dc.identifier.issn.none.fl_str_mv |
9783642229435 |
| dc.identifier.uri.none.fl_str_mv |
https://repositorio.escuelaing.edu.co/handle/001/1897 |
| identifier_str_mv |
9783642229442 9783642229435 |
| url |
https://repositorio.escuelaing.edu.co/handle/001/1897 |
| dc.language.iso.spa.fl_str_mv |
eng |
| language |
eng |
| dc.relation.ispartofseries.none.fl_str_mv |
Lecture Notes in Computer Science;6859 |
| dc.relation.citationendpage.spa.fl_str_mv |
406 |
| dc.relation.citationstartpage.spa.fl_str_mv |
400 |
| dc.relation.indexed.spa.fl_str_mv |
N/A |
| dc.relation.ispartofbook.eng.fl_str_mv |
Algebra and Coalgebra in Computer Science |
| dc.relation.references.spa.fl_str_mv |
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) 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) 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) Clavel, M., Palomino, M., Riesco, A.: Introducing the ITP tool: a tutorial. Journal of Universal Computer Science 12(11), 1618–1650 (2006) 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) Durán, F., Meseguer, J.: Maude’s module algebra. Science of Computer Programming 66(2), 125–153 (2007) 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) 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) 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) 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) Hendrix, J.: Decision Procedures for Equationally Based Reasoning. Ph.D. thesis. University of Illinois at Urbana-Champaign (2008) 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) 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 |
| dc.rights.eng.fl_str_mv |
© Springer-Verlag Berlin Heidelberg 2011 |
| dc.rights.coar.fl_str_mv |
http://purl.org/coar/access_right/c_14cb |
| dc.rights.uri.spa.fl_str_mv |
https://creativecommons.org/licenses/by/4.0/ |
| dc.rights.accessrights.spa.fl_str_mv |
info:eu-repo/semantics/closedAccess |
| dc.rights.creativecommons.spa.fl_str_mv |
Atribución 4.0 Internacional (CC BY 4.0) |
| rights_invalid_str_mv |
© Springer-Verlag Berlin Heidelberg 2011 https://creativecommons.org/licenses/by/4.0/ Atribución 4.0 Internacional (CC BY 4.0) http://purl.org/coar/access_right/c_14cb |
| eu_rights_str_mv |
closedAccess |
| dc.format.extent.spa.fl_str_mv |
7 páginas. |
| dc.format.mimetype.spa.fl_str_mv |
application/pdf |
| dc.publisher.spa.fl_str_mv |
Springer |
| dc.publisher.place.spa.fl_str_mv |
Berlín |
| institution |
Escuela Colombiana de Ingeniería Julio Garavito |
| bitstream.url.fl_str_mv |
https://repositorio.escuelaing.edu.co/bitstream/001/1897/6/Tool%20Interoperability%20in%20the%20Maude%20Formal%20Environment.png https://repositorio.escuelaing.edu.co/bitstream/001/1897/7/Tool%20Interoperability%20in%20the%20Maude%20Formal%20Environment.pdf.jpg https://repositorio.escuelaing.edu.co/bitstream/001/1897/1/Tool%20Interoperability%20in%20the%20Maude%20Formal%20Environment.pdf https://repositorio.escuelaing.edu.co/bitstream/001/1897/2/license.txt https://repositorio.escuelaing.edu.co/bitstream/001/1897/3/springer.pdf.txt https://repositorio.escuelaing.edu.co/bitstream/001/1897/5/Tool%20Interoperability%20in%20the%20Maude%20Formal%20Environment.pdf.txt |
| bitstream.checksum.fl_str_mv |
16217c50e606a15622d35ba756d11765 0dd3bc5e98e3ae5c1d80fa57d6ab0bae be9b098bc4d1ddfff3bec8d431433234 5a7ca94c2e5326ee169f979d71d0f06e d784fa8b6d98d27699781bd9a7cf19f0 d784fa8b6d98d27699781bd9a7cf19f0 |
| bitstream.checksumAlgorithm.fl_str_mv |
MD5 MD5 MD5 MD5 MD5 MD5 |
| repository.name.fl_str_mv |
Repositorio Escuela Colombiana de Ingeniería Julio Garavito |
| repository.mail.fl_str_mv |
repositorio.eci@escuelaing.edu.co |
| _version_ |
1808494286394621952 |
| spelling |
Durán, Francisco5002c334b7fc9f7b4b49cbacec064e0c600Rocha, Camiloebfd407af468605647a49186059da397600Álvarez, José Maríae51cc31bf714c23f2b7ffa8c350b6d00600Informática2021-12-03T17:29:14Z2021-12-03T17:29:14Z201197836422294429783642229435https://repositorio.escuelaing.edu.co/handle/001/1897We 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.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.7 páginas.application/pdfengSpringerBerlínLecture Notes in Computer Science;6859406400N/AAlgebra and Coalgebra in Computer ScienceClavel, 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)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)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)Clavel, M., Palomino, M., Riesco, A.: Introducing the ITP tool: a tutorial. Journal of Universal Computer Science 12(11), 1618–1650 (2006)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)Durán, F., Meseguer, J.: Maude’s module algebra. Science of Computer Programming 66(2), 125–153 (2007)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)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)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)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)Hendrix, J.: Decision Procedures for Equationally Based Reasoning. Ph.D. thesis. University of Illinois at Urbana-Champaign (2008)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)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© Springer-Verlag Berlin Heidelberg 2011https://creativecommons.org/licenses/by/4.0/info:eu-repo/semantics/closedAccessAtribución 4.0 Internacional (CC BY 4.0)http://purl.org/coar/access_right/c_14cbTool Interoperability in the Maude Formal EnvironmentCapítulo - Parte de Libroinfo:eu-repo/semantics/publishedVersionhttp://purl.org/coar/resource_type/c_3248http://purl.org/coar/resource_type/c_2df8fbb1Textinfo:eu-repo/semantics/bookParthttp://purl.org/redcol/resource_type/ARThttp://purl.org/coar/version/c_970fb48d4fbd8a85MaudePar críticoObligación de pruebaParte FuncionalHerramienta activaObjetivo de terminaciónCritical PairProof ObligationFunctional PartActive ToolTermination GoalTHUMBNAILTool Interoperability in the Maude Formal Environment.pngTool Interoperability in the Maude Formal Environment.pngimage/png111394https://repositorio.escuelaing.edu.co/bitstream/001/1897/6/Tool%20Interoperability%20in%20the%20Maude%20Formal%20Environment.png16217c50e606a15622d35ba756d11765MD56open accessTool Interoperability in the Maude Formal Environment.pdf.jpgTool Interoperability in the Maude Formal Environment.pdf.jpgGenerated Thumbnailimage/jpeg3473https://repositorio.escuelaing.edu.co/bitstream/001/1897/7/Tool%20Interoperability%20in%20the%20Maude%20Formal%20Environment.pdf.jpg0dd3bc5e98e3ae5c1d80fa57d6ab0baeMD57open accessORIGINALTool Interoperability in the Maude Formal Environment.pdfTool Interoperability in the Maude Formal Environment.pdfapplication/pdf189531https://repositorio.escuelaing.edu.co/bitstream/001/1897/1/Tool%20Interoperability%20in%20the%20Maude%20Formal%20Environment.pdfbe9b098bc4d1ddfff3bec8d431433234MD51open accessLICENSElicense.txtlicense.txttext/plain; charset=utf-81881https://repositorio.escuelaing.edu.co/bitstream/001/1897/2/license.txt5a7ca94c2e5326ee169f979d71d0f06eMD52open accessTEXTspringer.pdf.txtspringer.pdf.txtExtracted texttext/plain2https://repositorio.escuelaing.edu.co/bitstream/001/1897/3/springer.pdf.txtd784fa8b6d98d27699781bd9a7cf19f0MD53open accessTool Interoperability in the Maude Formal Environment.pdf.txtTool Interoperability in the Maude Formal Environment.pdf.txtExtracted texttext/plain2https://repositorio.escuelaing.edu.co/bitstream/001/1897/5/Tool%20Interoperability%20in%20the%20Maude%20Formal%20Environment.pdf.txtd784fa8b6d98d27699781bd9a7cf19f0MD55metadata only access001/1897oai:repositorio.escuelaing.edu.co:001/18972022-12-13 03:01:43.414open accessRepositorio Escuela Colombiana de Ingeniería Julio Garavitorepositorio.eci@escuelaing.edu.coU0kgVVNURUQgSEFDRSBQQVJURSBERUwgR1JVUE8gREUgUEFSRVMgRVZBTFVBRE9SRVMgREUgTEEgQ09MRUNDScOTTiAiUEVFUiBSRVZJRVciLCBPTUlUQSBFU1RBIExJQ0VOQ0lBLgoKQXV0b3Jpem8gYSBsYSBFc2N1ZWxhIENvbG9tYmlhbmEgZGUgSW5nZW5pZXLDrWEgSnVsaW8gR2FyYXZpdG8gcGFyYSBwdWJsaWNhciBlbCB0cmFiYWpvIGRlIGdyYWRvLCBhcnTDrWN1bG8sIHZpZGVvLCAKY29uZmVyZW5jaWEsIGxpYnJvLCBpbWFnZW4sIGZvdG9ncmFmw61hLCBhdWRpbywgcHJlc2VudGFjacOzbiB1IG90cm8gKGVuICAgIGFkZWxhbnRlIGRvY3VtZW50bykgcXVlIGVuIGxhIGZlY2hhIAplbnRyZWdvIGVuIGZvcm1hdG8gZGlnaXRhbCwgeSBsZSBwZXJtaXRvIGRlIGZvcm1hIGluZGVmaW5pZGEgcXVlIGxvIHB1YmxpcXVlIGVuIGVsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwsIAplbiBsb3MgdMOpcm1pbm9zIGVzdGFibGVjaWRvcyBlbiBsYSBMZXkgMjMgZGUgMTk4MiwgbGEgTGV5IDQ0IGRlIDE5OTMsIHkgZGVtw6FzIGxleWVzIHkganVyaXNwcnVkZW5jaWEgdmlnZW50ZQphbCByZXNwZWN0bywgcGFyYSBmaW5lcyBlZHVjYXRpdm9zIHkgbm8gbHVjcmF0aXZvcy4gRXN0YSBhdXRvcml6YWNpw7NuIGVzIHbDoWxpZGEgcGFyYSBsYXMgZmFjdWx0YWRlcyB5IGRlcmVjaG9zIGRlIAp1c28gc29icmUgbGEgb2JyYSBlbiBmb3JtYXRvIGRpZ2l0YWwsIGVsZWN0csOzbmljbywgdmlydHVhbDsgeSBwYXJhIHVzb3MgZW4gcmVkZXMsIGludGVybmV0LCBleHRyYW5ldCwgeSBjdWFscXVpZXIgCmZvcm1hdG8gbyBtZWRpbyBjb25vY2lkbyBvIHBvciBjb25vY2VyLgpFbiBtaSBjYWxpZGFkIGRlIGF1dG9yLCBleHByZXNvIHF1ZSBlbCBkb2N1bWVudG8gb2JqZXRvIGRlIGxhIHByZXNlbnRlIGF1dG9yaXphY2nDs24gZXMgb3JpZ2luYWwgeSBsbyBlbGFib3LDqSBzaW4gCnF1ZWJyYW50YXIgbmkgc3VwbGFudGFyIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBkZSB0ZXJjZXJvcy4gUG9yIGxvIHRhbnRvLCBlcyBkZSBtaSBleGNsdXNpdmEgYXV0b3LDrWEgeSwgZW4gY29uc2VjdWVuY2lhLCAKdGVuZ28gbGEgdGl0dWxhcmlkYWQgc29icmUgw6lsLiBFbiBjYXNvIGRlIHF1ZWphIG8gYWNjacOzbiBwb3IgcGFydGUgZGUgdW4gdGVyY2VybyByZWZlcmVudGUgYSBsb3MgZGVyZWNob3MgZGUgYXV0b3Igc29icmUgCmVsIGRvY3VtZW50byBlbiBjdWVzdGnDs24sIGFzdW1pcsOpIGxhIHJlc3BvbnNhYmlsaWRhZCB0b3RhbCB5IHNhbGRyw6kgZW4gZGVmZW5zYSBkZSBsb3MgZGVyZWNob3MgYXF1w60gYXV0b3JpemFkb3MuIEVzdG8gCnNpZ25pZmljYSBxdWUsIHBhcmEgdG9kb3MgbG9zIGVmZWN0b3MsIGxhIEVzY3VlbGEgYWN0w7phIGNvbW8gdW4gdGVyY2VybyBkZSBidWVuYSBmZS4KVG9kYSBwZXJzb25hIHF1ZSBjb25zdWx0ZSBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIEVzY3VlbGEsIGVsIENhdMOhbG9nbyBlbiBsw61uZWEgdSBvdHJvIG1lZGlvIGVsZWN0csOzbmljbywgCnBvZHLDoSBjb3BpYXIgYXBhcnRlcyBkZWwgdGV4dG8sIGNvbiBlbCBjb21wcm9taXNvIGRlIGNpdGFyIHNpZW1wcmUgbGEgZnVlbnRlLCBsYSBjdWFsIGluY2x1eWUgZWwgdMOtdHVsbyBkZWwgdHJhYmFqbyB5IGVsIAphdXRvci5Fc3RhIGF1dG9yaXphY2nDs24gbm8gaW1wbGljYSByZW51bmNpYSBhIGxhIGZhY3VsdGFkIHF1ZSB0ZW5nbyBkZSBwdWJsaWNhciB0b3RhbCBvIHBhcmNpYWxtZW50ZSBsYSBvYnJhIGVuIG90cm9zIAptZWRpb3MuRXN0YSBhdXRvcml6YWNpw7NuIGVzdMOhIHJlc3BhbGRhZGEgcG9yIGxhcyBmaXJtYXMgZGVsIChsb3MpIGF1dG9yKGVzKSBkZWwgZG9jdW1lbnRvLiAKU8OtIGF1dG9yaXpvIChhbWJvcykK |