Programming and symbolic computation in Maude
RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia
JavaScript is disabled for your browser. Some features of this site may not work without it.
Buscar en RiuNet
Listar
Mi cuenta
Estadísticas
Ayuda RiuNet
Admin. UPV
Programming and symbolic computation in Maude
Mostrar el registro sencillo del ítem
Ficheros en el ítem
![[Cerrado]](/themes/UPV/images/candado.png)
| dc.contributor.author | Durán, Francisco
|
es_ES |
| dc.contributor.author | Eker, Steven
|
es_ES |
| dc.contributor.author | Escobar Román, Santiago
|
es_ES |
| dc.contributor.author | NARCISO MARTÍ OLIET
|
es_ES |
| dc.contributor.author | José Meseguer
|
es_ES |
| dc.contributor.author | Rubén Rubio
|
es_ES |
| dc.contributor.author | Talcott, Carolyn
|
es_ES |
| dc.date.accessioned | 2021-07-29T03:30:53Z | |
| dc.date.available | 2021-07-29T03:30:53Z | |
| dc.date.issued | 2020-01 | es_ES |
| dc.identifier.issn | 2352-2208 | es_ES |
| dc.identifier.uri | http://hdl.handle.net/10251/170775 | |
| dc.description.abstract | [EN] Rewriting logic is both a flexible semantic framework within which widely different concurrent systems can be naturally specified and a logical framework in which widely different logics can be specified. Maude programs are exactly rewrite theories. Maude has also a formal environment of verification tools. Symbolic computation is a powerful technique for reasoning about the correctness of concurrent systems and for increasing the power of formal tools. We present several new symbolic features of Maude that enhance formal reasoning about Maude programs and the effectiveness of formal tools. They include: (i) very general unification modulo user-definable equational theories, and (ii) symbolic reachability analysis of concurrent systems using narrowing. The paper does not focus just on symbolic features: it also describes several other new Maude features, including: (iii) Maude's strategy language for controlling rewriting, and (iv) external objects that allow flexible interaction of Maude object-based concurrent systems with the external world. In particular, meta-interpreters are external objects encapsulating Maude interpreters that can interact with many other objects. To make the paper self-contained and give a reasonably complete language overview, we also review the basic Maude features for equational rewriting and rewriting with rules, Maude programming of concurrent object systems, and reflection. Furthermore, we include many examples illustrating all the Maude notions and features described in the paper. | es_ES |
| dc.description.sponsorship | Duran has been partially supported by MINECO/FEDER project TIN2014-52034-R. Escobar has been partially supported by the EU (FEDER) and the MCIU under grant RTI2018-094403-B-C32, by the Spanish Generalitat Valenciana under grant PROMETE0/2019/098, and by the US Air Force Office of Scientific Research under award number FA9550-17-1-0286. MartiOliet and Rubio have been partially supported by MCIU Spanish project TRACES (TIN2015-67522-C3-3-R). Rubio has also been partially supported by a MCIU grant FPU17/02319. Meseguer and Talcott have been partially supported by NRL Grant N00173 -17-1-G002. Talcott has also been partially supported by ONR Grant N00014-15-1-2202. | es_ES |
| dc.language | Inglés | es_ES |
| dc.publisher | Elsevier | es_ES |
| dc.relation.ispartof | Journal of Logical and Algebraic Methods in Programming | es_ES |
| dc.rights | Reconocimiento - No comercial - Sin obra derivada (by-nc-nd) | es_ES |
| dc.subject | Maude and rewriting logic | es_ES |
| dc.subject | Strategies | es_ES |
| dc.subject | External objects | es_ES |
| dc.subject | Unification and narrowing | es_ES |
| dc.subject | Symbolic model checking | es_ES |
| dc.subject | Meta-interpreters | es_ES |
| dc.subject.classification | LENGUAJES Y SISTEMAS INFORMATICOS | es_ES |
| dc.title | Programming and symbolic computation in Maude | es_ES |
| dc.type | Artículo | es_ES |
| dc.identifier.doi | 10.1016/j.jlamp.2019.100497 | es_ES |
| dc.relation.projectID | info:eu-repo/grantAgreement/MINECO//TIN2014-52034-R/ES/UN MARCO DIRIGIDO POR MODELOS PARA EL DISEÑO E INTEGRACION DE SISTEMAS DE GESTION DE INFRAESTRUCTURAS/ | es_ES |
| dc.relation.projectID | info:eu-repo/grantAgreement/AFOSR//FA9550-17-1-0266/US/Advanced symbolic methods for the cryptographic protocol analyzer Maude-NPA/ | es_ES |
| dc.relation.projectID | info:eu-repo/grantAgreement/MECD//FPU17%2F02319/ | es_ES |
| dc.relation.projectID | info:eu-repo/grantAgreement/ONR//N00014-15-1-2202/ | es_ES |
| dc.relation.projectID | info:eu-repo/grantAgreement/NRL//N00173-17-1-G002/ | es_ES |
| dc.relation.projectID | info:eu-repo/grantAgreement/MINECO//TIN2015-67522-C3-3-R/ES/TECNOLOGIAS Y HERRAMIENTAS PARA EL DESARROLLO DE SOFTWARE CONSCIENTE DE LOS RECURSOS, CORRECTO Y EFICIENTE/ | es_ES |
| dc.relation.projectID | info:eu-repo/grantAgreement/AFOSR//FA9550-17-1-0286/ | es_ES |
| dc.relation.projectID | info:eu-repo/grantAgreement/GVA//PROMETEO%2F2019%2F098/ES/DeepTrust: Deep Logic Technology for Software Trustworthiness/ | es_ES |
| dc.relation.projectID | info:eu-repo/grantAgreement/GVA//PROMETEOII%2F2015%2F013/ES/SmartLogic: Logic Technologies for Software Security and Performance/ | es_ES |
| dc.relation.projectID | info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020/RTI2018-094403-B-C32/ES/RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES/ | es_ES |
| dc.rights.accessRights | Abierto | es_ES |
| dc.contributor.affiliation | Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació | es_ES |
| dc.description.bibliographicCitation | Durán, F.; Eker, S.; Escobar Román, S.; NARCISO MARTÍ OLIET; José Meseguer; Rubén Rubio; Talcott, C. (2020). Programming and symbolic computation in Maude. Journal of Logical and Algebraic Methods in Programming. 110:1-58. https://doi.org/10.1016/j.jlamp.2019.100497 | es_ES |
| dc.description.accrualMethod | S | es_ES |
| dc.relation.publisherversion | https://doi.org/10.1016/j.jlamp.2019.100497 | es_ES |
| dc.description.upvformatpinicio | 1 | es_ES |
| dc.description.upvformatpfin | 58 | es_ES |
| dc.type.version | info:eu-repo/semantics/publishedVersion | es_ES |
| dc.description.volume | 110 | es_ES |
| dc.relation.pasarela | S\401108 | es_ES |
| dc.contributor.funder | Generalitat Valenciana | es_ES |
| dc.contributor.funder | U.S. Naval Research Laboratory | es_ES |
| dc.contributor.funder | Agencia Estatal de Investigación | es_ES |
| dc.contributor.funder | European Regional Development Fund | es_ES |
| dc.contributor.funder | AIR FORCE OFFICE OF SCIENTIFIC RESEARCH | es_ES |
| dc.contributor.funder | Ministerio de Economía y Competitividad | es_ES |
| dc.contributor.funder | Ministerio de Educación, Cultura y Deporte | es_ES |
| dc.description.references | Alpuente, M., Escobar, S., Espert, J., & Meseguer, J. (2014). A modular order-sorted equational generalization algorithm. Information and Computation, 235, 98-136. doi:10.1016/j.ic.2014.01.006 | es_ES |
| dc.description.references | K. Bae, J. Meseguer, Predicate abstraction of rewrite theories, in: [36], 2014, pp. 61–76. | es_ES |
| dc.description.references | Bae, K., & Meseguer, J. (2015). Model checking linear temporal logic of rewriting formulas under localized fairness. Science of Computer Programming, 99, 193-234. doi:10.1016/j.scico.2014.02.006 | es_ES |
| dc.description.references | Bae, K., Meseguer, J., & Ölveczky, P. C. (2014). Formal patterns for multirate distributed real-time systems. Science of Computer Programming, 91, 3-44. doi:10.1016/j.scico.2013.09.010 | es_ES |
| dc.description.references | P. Borovanský, C. Kirchner, H. Kirchner, P.E. Moreau, C. Ringeissen, An overview of ELAN, in: [77], 1998, pp. 55–70. | es_ES |
| dc.description.references | Bouhoula, A., Jouannaud, J.-P., & Meseguer, J. (2000). Specification and proof in membership equational logic. Theoretical Computer Science, 236(1-2), 35-132. doi:10.1016/s0304-3975(99)00206-6 | es_ES |
| dc.description.references | Bravenboer, M., Kalleberg, K. T., Vermaas, R., & Visser, E. (2008). Stratego/XT 0.17. A language and toolset for program transformation. Science of Computer Programming, 72(1-2), 52-70. doi:10.1016/j.scico.2007.11.003 | es_ES |
| dc.description.references | Bruni, R., & Meseguer, J. (2006). Semantic foundations for generalized rewrite theories. Theoretical Computer Science, 360(1-3), 386-414. doi:10.1016/j.tcs.2006.04.012 | es_ES |
| dc.description.references | M. Clavel, F. Durán, S. Eker, S. Escobar, P. Lincoln, N. Martí-Oliet, C.L. Talcott, Two decades of Maude, in: [86], 2015, pp. 232–254. | es_ES |
| dc.description.references | Clavel, M., Durán, F., Eker, S., Lincoln, P., Martı́-Oliet, N., Meseguer, J., & Quesada, J. F. (2002). Maude: specification and programming in rewriting logic. Theoretical Computer Science, 285(2), 187-243. doi:10.1016/s0304-3975(01)00359-0 | es_ES |
| dc.description.references | Clavel, M., & Meseguer, J. (2002). Reflection in conditional rewriting logic. Theoretical Computer Science, 285(2), 245-288. doi:10.1016/s0304-3975(01)00360-7 | es_ES |
| dc.description.references | F. Durán, S. Eker, S. Escobar, N. Martí-Oliet, J. Meseguer, C.L. Talcott, Associative unification and symbolic reasoning modulo associativity in Maude, in: [121], 2018, pp. 98–114. | es_ES |
| dc.description.references | Durán, F., Lucas, S., Marché, C., Meseguer, J., & Urbain, X. (2008). Proving operational termination of membership equational programs. Higher-Order and Symbolic Computation, 21(1-2), 59-88. doi:10.1007/s10990-008-9028-2 | es_ES |
| dc.description.references | F. Durán, J. Meseguer, An extensible module algebra for Maude, in: [77], 1998, pp. 174–195. | es_ES |
| dc.description.references | Durán, F., & Meseguer, J. (2003). Structured theories and institutions. Theoretical Computer Science, 309(1-3), 357-380. doi:10.1016/s0304-3975(03)00312-8 | es_ES |
| dc.description.references | Durán, F., & Meseguer, J. (2007). Maude’s module algebra. Science of Computer Programming, 66(2), 125-153. doi:10.1016/j.scico.2006.07.002 | es_ES |
| dc.description.references | Durán, F., & Meseguer, J. (2012). On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. The Journal of Logic and Algebraic Programming, 81(7-8), 816-850. doi:10.1016/j.jlap.2011.12.004 | es_ES |
| dc.description.references | F. Durán, P.C. Ölveczky, A guide to extending Full Maude illustrated with the implementation of Real-Time Maude, in: [116], 2009, pp. 83–102. | es_ES |
| dc.description.references | S. Escobar, Multi-paradigm programming in Maude, in: [121], 2018, pp. 26–44. | es_ES |
| dc.description.references | Escobar, S., Meadows, C., Meseguer, J., & Santiago, S. (2014). State space reduction in the Maude-NRL Protocol Analyzer. Information and Computation, 238, 157-186. doi:10.1016/j.ic.2014.07.007 | es_ES |
| dc.description.references | Escobar, S., Sasse, R., & Meseguer, J. (2012). Folding variant narrowing and optimal variant termination. The Journal of Logic and Algebraic Programming, 81(7-8), 898-928. doi:10.1016/j.jlap.2012.01.002 | es_ES |
| dc.description.references | H. Garavel, M. Tabikh, I. Arrada, Benchmarking implementations of term rewriting and pattern matching in algebraic, functional, and object-oriented languages – the 4th rewrite engines competition, in: [121], 2018, pp. 1–25. | es_ES |
| dc.description.references | Goguen, J. A., & Burstall, R. M. (1992). Institutions: abstract model theory for specification and programming. Journal of the ACM, 39(1), 95-146. doi:10.1145/147508.147524 | es_ES |
| dc.description.references | Goguen, J. A., & Meseguer, J. (1984). Equality, types, modules, and (why not?) generics for logic programming. The Journal of Logic Programming, 1(2), 179-210. doi:10.1016/0743-1066(84)90004-9 | es_ES |
| dc.description.references | Goguen, J. A., & Meseguer, J. (1992). Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science, 105(2), 217-273. doi:10.1016/0304-3975(92)90302-v | es_ES |
| dc.description.references | R. Gutiérrez, J. Meseguer, Variant-based decidable satisfiability in initial algebras with predicates, in: [61], 2018, pp. 306–322. | es_ES |
| dc.description.references | Gutiérrez, R., Meseguer, J., & Rocha, C. (2015). Order-sorted equality enrichments modulo axioms. Science of Computer Programming, 99, 235-261. doi:10.1016/j.scico.2014.07.003 | es_ES |
| dc.description.references | Horn, A. (1951). On sentences which are true of direct unions of algebras. Journal of Symbolic Logic, 16(1), 14-21. doi:10.2307/2268661 | es_ES |
| dc.description.references | Katelman, M., Keller, S., & Meseguer, J. (2012). Rewriting semantics of production rule sets. The Journal of Logic and Algebraic Programming, 81(7-8), 929-956. doi:10.1016/j.jlap.2012.06.002 | es_ES |
| dc.description.references | Kowalski, R. (1979). Algorithm = logic + control. Communications of the ACM, 22(7), 424-436. doi:10.1145/359131.359136 | es_ES |
| dc.description.references | Lucanu, D., Rusu, V., & Arusoaie, A. (2017). A generic framework for symbolic execution: A coinductive approach. Journal of Symbolic Computation, 80, 125-163. doi:10.1016/j.jsc.2016.07.012 | es_ES |
| dc.description.references | D. Lucanu, V. Rusu, A. Arusoaie, D. Nowak, Verifying reachability-logic properties on rewriting-logic specifications, in: [86], 2015, pp. 451–474. | es_ES |
| dc.description.references | Lucas, S., & Meseguer, J. (2016). Normal forms and normal theories in conditional rewriting. Journal of Logical and Algebraic Methods in Programming, 85(1), 67-97. doi:10.1016/j.jlamp.2015.06.001 | es_ES |
| dc.description.references | N. Martí-Oliet, J. Meseguer, A. Verdejo, A rewriting semantics for Maude strategies, in: [116], 2009, pp. 227–247. | es_ES |
| dc.description.references | Martí-Oliet, N., Palomino, M., & Verdejo, A. (2007). Strategies and simulations in a semantic framework. Journal of Algorithms, 62(3-4), 95-116. doi:10.1016/j.jalgor.2007.04.002 | es_ES |
| dc.description.references | Meseguer, J. (1992). Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1), 73-155. doi:10.1016/0304-3975(92)90182-f | es_ES |
| dc.description.references | Meseguer, J. (2012). Twenty years of rewriting logic. The Journal of Logic and Algebraic Programming, 81(7-8), 721-781. doi:10.1016/j.jlap.2012.06.003 | es_ES |
| dc.description.references | Meseguer, J. (2017). Strict coherence of conditional rewriting modulo axioms. Theoretical Computer Science, 672, 1-35. doi:10.1016/j.tcs.2016.12.026 | es_ES |
| dc.description.references | J. Meseguer, Generalized rewrite theories and coherence completion, in: [121], 2018, pp. 164–183. | es_ES |
| dc.description.references | Meseguer, J. (2018). Variant-based satisfiability in initial algebras. Science of Computer Programming, 154, 3-41. doi:10.1016/j.scico.2017.09.001 | es_ES |
| dc.description.references | Meseguer, J., Goguen, J. A., & Smolka, G. (1989). Order-sorted unification. Journal of Symbolic Computation, 8(4), 383-413. doi:10.1016/s0747-7171(89)80036-7 | es_ES |
| dc.description.references | Meseguer, J., & Ölveczky, P. C. (2012). Formalization and correctness of the PALS architectural pattern for distributed real-time systems. Theoretical Computer Science, 451, 1-37. doi:10.1016/j.tcs.2012.05.040 | es_ES |
| dc.description.references | Meseguer, J., Palomino, M., & Martí-Oliet, N. (2008). Equational abstractions. Theoretical Computer Science, 403(2-3), 239-264. doi:10.1016/j.tcs.2008.04.040 | es_ES |
| dc.description.references | Meseguer, J., & Roşu, G. (2007). The rewriting logic semantics project. Theoretical Computer Science, 373(3), 213-237. doi:10.1016/j.tcs.2006.12.018 | es_ES |
| dc.description.references | Meseguer, J., & Roşu, G. (2013). The rewriting logic semantics project: A progress report. Information and Computation, 231, 38-69. doi:10.1016/j.ic.2013.08.004 | es_ES |
| dc.description.references | Meseguer, J., & Skeirik, S. (2017). Equational formulas and pattern operations in initial order-sorted algebras. Formal Aspects of Computing, 29(3), 423-452. doi:10.1007/s00165-017-0415-5 | es_ES |
| dc.description.references | Meseguer, J., & Thati, P. (2007). Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Higher-Order and Symbolic Computation, 20(1-2), 123-160. doi:10.1007/s10990-007-9000-6 | es_ES |
| dc.description.references | C. Olarte, E. Pimentel, C. Rocha, Proving structural properties of sequent systems in rewriting logic, in: [121], 2018, pp. 115–135. | es_ES |
| dc.description.references | Ölveczky, P. C., & Meseguer, J. (2007). Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation, 20(1-2), 161-196. doi:10.1007/s10990-007-9001-5 | es_ES |
| dc.description.references | Ölveczky, P. C., & Thorvaldsen, S. (2009). Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude. Theoretical Computer Science, 410(2-3), 254-280. doi:10.1016/j.tcs.2008.09.022 | es_ES |
| dc.description.references | Rocha, C., Meseguer, J., & Muñoz, C. (2017). Rewriting modulo SMT and open system analysis. Journal of Logical and Algebraic Methods in Programming, 86(1), 269-297. doi:10.1016/j.jlamp.2016.10.001 | es_ES |
| dc.description.references | Şerbănuţă, T. F., Roşu, G., & Meseguer, J. (2009). A rewriting logic approach to operational semantics. Information and Computation, 207(2), 305-340. doi:10.1016/j.ic.2008.03.026 | es_ES |
| dc.description.references | Skeirik, S., & Meseguer, J. (2018). Metalevel algorithms for variant satisfiability. Journal of Logical and Algebraic Methods in Programming, 96, 81-110. doi:10.1016/j.jlamp.2017.12.006 | es_ES |
| dc.description.references | S. Skeirik, A. Ştefănescu, J. Meseguer, A constructor-based reachability logic for rewrite theories, in: [61], 2018, pp. 201–217. | es_ES |
| dc.description.references | Strachey, C. (2000). Higher-Order and Symbolic Computation, 13(1/2), 11-49. doi:10.1023/a:1010000313106 | es_ES |
| dc.description.references | A. Ştefănescu, S. Ciobâcă, R. Mereuta, B.M. Moore, T. Serbanuta, G. Roşu, All-path reachability logic, in: [36], 2014, pp. 425–440. | es_ES |
| dc.description.references | Tushkanova, E., Giorgetti, A., Ringeissen, C., & Kouchnarenko, O. (2015). A rule-based system for automatic decidability and combinability. Science of Computer Programming, 99, 3-23. doi:10.1016/j.scico.2014.02.005 | es_ES |
Este ítem aparece en la(s) siguiente(s) colección(ones)
Universitat Politècnica de València. Unidad de Documentación Científica de la Biblioteca (+34) 96 387 70 85 · RiuNet@bib.upv.es
El contenido de este sitio está bajo una licencia Creative Commons Reconocimiento – No Comercial – Sin Obra Derivada (by-nc-nd), salvo que se indique lo contrario.
Los metadatos de este sitio están bajo una licencia Dominio Público.
