{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T22:00:47Z","timestamp":1747173647959,"version":"3.40.5"},"reference-count":18,"publisher":"Cambridge University Press (CUP)","issue":"5-6","license":[{"start":{"date-parts":[[2019,9,20]],"date-time":"2019-09-20T00:00:00Z","timestamp":1568937600000},"content-version":"unspecified","delay-in-days":19,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2019,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Concurrent functional languages that are endowed with symbolic reasoning capabilities such as Maude offer a high-level, elegant, and efficient approach to programming and analyzing complex, highly nondeterministic software systems. Maude\u2019s symbolic capabilities are based on equational unification and narrowing in rewrite theories, and provide Maude with advanced logic programming capabilities such as unification modulo user-definable equational theories and symbolic reachability analysis in rewrite theories. Intricate computing problems may be effectively and naturally solved in Maude thanks to the synergy of these recently developed symbolic capabilities and classical Maude features, such as: (i) rich type structures with sorts (types), subsorts, and overloading; (ii) equational rewriting modulo various combinations of axioms such as associativity, commutativity, and identity; and (iii) classical reachability analysis in rewrite theories. However, the combination of all of these features may hinder the understanding of Maude symbolic computations for non-experienced developers. The purpose of this article is to describe how programming and analysis of Maude rewrite theories can be made easier by providing a sophisticated graphical tool called Narval that supports the fine-grained inspection of Maude symbolic computations.<\/jats:p>","DOI":"10.1017\/s1471068419000243","type":"journal-article","created":{"date-parts":[[2019,9,20]],"date-time":"2019-09-20T13:06:21Z","timestamp":1568984781000},"page":"874-890","source":"Crossref","is-referenced-by-count":2,"title":["Symbolic Analysis of Maude Theories with Narval"],"prefix":"10.1017","volume":"19","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9268-1178","authenticated-orcid":false,"given":"MAR\u00cdA","family":"ALPUENTE","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"SANTIAGO","family":"ESCOBAR","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2994-6986","authenticated-orcid":false,"given":"JULIA","family":"SAPI\u00d1A","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"DEMIS","family":"BALLIS","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2019,9,20]]},"reference":[{"key":"S1471068419000243_ref11","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/978-3-642-37651-1_6","volume-title":"Programming Logics - Essays in Memory of Harald Ganzinger","volume":"7797","author":"Hanus","year":"2013"},{"key":"S1471068419000243_ref5","unstructured":"Clavel, M. , Dur\u00e1n, F. , Eker, S. , Escobar, S. , Lincoln, P. , Mart\u00ed-Oliet, N. , Meseguer, J. , and Talcott, C. 2016. Maude Manual (Version 2.7.1). Tech. rep., SRI International Computer Science Laboratory. Available at: http:\/\/maude.cs.uiuc.edu\/maude2-manual\/."},{"key":"S1471068419000243_ref14","unstructured":"Mau-Dev 2016. The Mau-Dev Website. Available at: http:\/\/safe-tools.dsic.upv.es\/maudev."},{"key":"S1471068419000243_ref2","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1017\/S1471068416000375","article-title":"Assertion-based Analysis via Slicing with ABETS","volume":"5\u20136","author":"Alpuente","year":"2016","journal-title":"Theory and Practice of Logic Programming 16"},{"key":"S1471068419000243_ref7","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/978-3-319-99840-4_6","volume-title":"Proceedings of the 12th International Workshop on Rewriting Logic and its Applications","volume":"11152","author":"Dur\u00e1n","year":"2018"},{"key":"S1471068419000243_ref3","unstructured":"Alpuente, M. , Ballis, D. , and Sapi\u00f1a, J. 2019. Static Correction of Maude Programs with Assertions. Journal of Systems and Software 153, 64\u201385."},{"volume-title":"All About Maude: A High-Performance Logical Framework","year":"2007","author":"Clavel","key":"S1471068419000243_ref6"},{"key":"S1471068419000243_ref9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-319-99840-4_1","volume-title":"Proceedings of the 12th International Workshop on Rewriting Logic and its Applications (WRLA 2018)","volume":"11152","author":"Garavel","year":"2018"},{"key":"S1471068419000243_ref17","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/978-3-662-57669-4_2","volume-title":"Proceedings of the 25th International Workshop on Logic, Language, Information, and Computation (WoLLIC 2018)","volume":"10944","author":"Meseguer","year":"2018"},{"key":"S1471068419000243_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.01.002"},{"key":"S1471068419000243_ref1","unstructured":"Alpuente, M. , Ballis, D. , Frechina, F. , and Sapi\u00f1a, J. 2015. Exploring Conditional Rewriting Logic Computations. Journal of Symbolic Computation 69, 3\u201339."},{"key":"S1471068419000243_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/S147106841700031X"},{"key":"S1471068419000243_ref10","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/1858996.1859022","volume-title":"Proceedings of the 25th IEEE\/ACM International Conference on Automated Software Engineering (ASE 2010)","author":"H\u00e4hnle","year":"2010"},{"key":"S1471068419000243_ref12","first-page":"1","volume-title":"Proceedings of the 8th International Conference on Software Testing, Verification and Validation (ICST 2015)","author":"Honfi","year":"2015"},{"key":"S1471068419000243_ref13","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","article-title":"Symbolic Execution and Program Testing","volume":"7","author":"King","year":"1976","journal-title":"Communications of the ACM 19"},{"key":"S1471068419000243_ref15","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","article-title":"Conditional Rewriting Logic as a Unified Model of Concurrency","volume":"1","author":"Meseguer","year":"1992","journal-title":"Theoretical Computer Science 96"},{"key":"S1471068419000243_ref16","doi-asserted-by":"crossref","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","article-title":"Twenty Years of Rewriting Logic","volume":"7","author":"Meseguer","year":"2012","journal-title":"The Journal of Logic and Algebraic Programming 81"},{"key":"S1471068419000243_ref18","first-page":"244","volume-title":"Proceedings of the 3rd International Conference on Algebraic and Logic Programming (ALP 1992)","volume":"632","author":"Middeldorp","year":"1992"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068419000243","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,21]],"date-time":"2021-01-21T18:07:35Z","timestamp":1611252455000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068419000243\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9]]},"references-count":18,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2019,9]]}},"alternative-id":["S1471068419000243"],"URL":"https:\/\/doi.org\/10.1017\/s1471068419000243","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2019,9]]}}}