{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,29]],"date-time":"2026-07-29T02:21:33Z","timestamp":1785291693749,"version":"3.55.0"},"reference-count":79,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2022,2,11]],"date-time":"2022-02-11T00:00:00Z","timestamp":1644537600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2022,5]]},"abstract":"Abstract<\/jats:title>This paper introduces$\\tt{{Presto}}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, a symbolic partial evaluator for Maude\u2019s rewriting logic theories that can improve system analysis and verification. In$\\tt{{Presto}}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, the automated optimization of a conditional rewrite theory$\\mathcal{R}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>(whose rules define the concurrent transitions of a system) is achieved by partially evaluating, with respect to the rules of$\\mathcal{R}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, an underlying, companion equational logic theory$\\mathcal{E}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>that specifies the algebraic structure of the system states of$\\mathcal{R}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. This can be particularly useful for specializing an overly general equational theory$\\mathcal{E}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>whose operators may obey complex combinations of associativity, commutativity, and\/or identity axioms, when being plugged into a host rewrite theory$\\mathcal{R}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>as happens, for instance, in protocol analysis, where sophisticated equational theories for cryptography are used.$\\tt{{Presto}}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>implements different unfolding operators that are based onfolding variant narrowing<\/jats:italic>(the symbolic engine of Maude\u2019s equational theories). When combined with an appropriate abstraction algorithm, they allow the specialization to be adapted to the theory termination behavior and bring significant improvement while ensuring strong correctness and termination of the specialization. We demonstrate the effectiveness of$\\tt{{Presto}}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>in several examples of protocol analysis where it achieves a significant speed-up. Actually, the transformation provided by$\\tt{{Presto}}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>may cut down an infinite folding variant narrowing space to a finite one, and moreover, some of the costly algebraic axioms and rule conditions may be eliminated as well. As far as we know, this is the first partial evaluator for Maude that respects the semantics of functional, logic, concurrent, and object-oriented computations.<\/jats:p>","DOI":"10.1017\/s1471068421000600","type":"journal-article","created":{"date-parts":[[2022,2,11]],"date-time":"2022-02-11T13:44:36Z","timestamp":1644587076000},"page":"444-495","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":1,"title":["Symbolic Specialization of Rewriting Logic Theories withPresto<\/tt>"],"prefix":"10.1017","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9268-1178","authenticated-orcid":false,"given":"MAR\u00cdA","family":"ALPUENTE","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"SANTIAGO","family":"ESCOBAR","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2994-6986","authenticated-orcid":false,"given":"JULIA","family":"SAPI\u00d1A","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"DEMIS","family":"BALLIS","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2022,2,11]]},"reference":[{"key":"S1471068421000600_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2019.03.061"},{"key":"S1471068421000600_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.01.006"},{"key":"S1471068421000600_ref35","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"S1471068421000600_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/291891.291896"},{"key":"S1471068421000600_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73449-9_13"},{"key":"S1471068421000600_ref33","volume-title":"All About Maude: A High-Performance Logical Framework","author":"Clavel","year":"2007"},{"key":"S1471068421000600_ref44","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.01.002"},{"key":"S1471068421000600_ref48","doi-asserted-by":"crossref","unstructured":"Garavel, H. , Tabikh, M. , and Arrada, I. (2018). Benchmarking Implementations of Term Rewriting and Pattern Matching in Algebraic, Functional, and Object-Oriented Languages - The 4th Rewrite Engines Competition. In Proceedings of the 12th International Workshop on Rewriting Logic and its Applications (WRLA 2018), volume 11152 of Lecture Notes in Computer Science, pages 1\u201325. Springer.","DOI":"10.1007\/978-3-319-99840-4_1"},{"key":"S1471068421000600_ref69","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.04.040"},{"key":"S1471068421000600_ref79","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00366-8"},{"key":"S1471068421000600_ref57","doi-asserted-by":"publisher","DOI":"10.1145\/351268.351298"},{"key":"S1471068421000600_ref71","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_23"},{"key":"S1471068421000600_ref77","doi-asserted-by":"publisher","DOI":"10.1145\/321850.321859"},{"key":"S1471068421000600_ref34","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.66.8"},{"key":"S1471068421000600_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-020-00455-3"},{"key":"S1471068421000600_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068419000243"},{"key":"S1471068421000600_ref58","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(91)90027-M"},{"key":"S1471068421000600_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-19570-0_11"},{"key":"S1471068421000600_ref17","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2020-1991"},{"key":"S1471068421000600_ref51","unstructured":"Hanus, M. and Peem\u00f6ller, B. (2014). A Partial Evaluator for Curry. In Proceedings of the 28th International Workshop on (Constraint) Logic Programming (WLP 2014), volume 1335, pages 155\u2013171. CEUR-WS.org."},{"key":"S1471068421000600_ref67","first-page":"110","article-title":"Generalized Rewrite Theories, Coherence Completion, and Symbolic Methods","author":"Meseguer","year":"2020","journal-title":"Journal of Logical and Algebraic Methods in Programming"},{"key":"S1471068421000600_ref76","doi-asserted-by":"crossref","unstructured":"Serbanuta, T.-F. and Rosu, G. (2006). Computationally Equivalent Elimination of Conditions. In Proceedings of the 17th International Conference on Rewriting Techniques and Applications (RTA 2006), volume 4098 of Lecture Notes in Computer Science, pages 19\u201334. Springer.","DOI":"10.1007\/11805618_3"},{"key":"S1471068421000600_ref40","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.100513"},{"key":"S1471068421000600_ref46","doi-asserted-by":"publisher","DOI":"10.1145\/154630.154640"},{"key":"S1471068421000600_ref72","unstructured":"Peem\u00e6ller, B. (2017). Normalization and Partial Evaluation of Functional Logic Programs. PhD thesis, University of Kiel, Germany."},{"key":"S1471068421000600_ref78","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57880-3_32"},{"key":"S1471068421000600_ref54","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49727-7_14"},{"key":"S1471068421000600_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2009.04.016"},{"key":"S1471068421000600_ref45","unstructured":"Fay, M. (1979). First Order Unification in an Equational Theory. In Proceedings of the 4th International Conference on Automated Deduction (CADE 1979), pages 161\u2013167. Academic Press, Inc."},{"key":"S1471068421000600_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40885-4_23"},{"key":"S1471068421000600_ref32","unstructured":"Clavel, M. , Dur\u00e1n, F. , Eker, S. , Escobar, S. , Lincoln, P. , Mart\u00ed-Oliet, N. , Meseguer, J. , Rubio, R. , and Talcott, C. (2020). Maude Manual (Version 3.0). Technical report, SRI International Computer Science Laboratory. Available at: http:\/\/maude.cs.uiuc.edu."},{"key":"S1471068421000600_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28717-6_8"},{"key":"S1471068421000600_ref50","doi-asserted-by":"publisher","DOI":"10.1145\/251595.251602"},{"key":"S1471068421000600_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.100501"},{"key":"S1471068421000600_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.07.037"},{"key":"S1471068421000600_ref20","doi-asserted-by":"crossref","unstructured":"Alpuente, M. , Escobar, S. , Meseguer, J. , and Ojeda, P. (2008). A Modular Equational Generalization Algorithm. In Proceedings of the 18th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2008), volume 5438 of Lecture Notes in Computer Science, pages 24\u201339. Springer.","DOI":"10.1007\/978-3-642-00515-2_3"},{"key":"S1471068421000600_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.07.014"},{"key":"S1471068421000600_ref53","doi-asserted-by":"crossref","unstructured":"J\u00f8rgensen, J. , Leuschel, M. , and Martens, B. (1996). Conjunctive Partial Deduction in Practice. In Proceedings of the 6th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 1996), volume 1207 of Lecture Notes in Computer Science, pages 59\u201382. Springer.","DOI":"10.1007\/3-540-62718-9_5"},{"key":"S1471068421000600_ref56","doi-asserted-by":"crossref","unstructured":"Leuschel, M. and Gruner, S. (2001). Abstract Conjunctive Partial Deduction Using Regular Types and Its Application to Model Checking. In Proceedings of the 11th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2001), volume 2372 of Lecture Notes in Computer Science, pages 91\u2013110. Springer.","DOI":"10.1007\/3-540-45607-4_6"},{"key":"S1471068421000600_ref68","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-68446-4_1"},{"key":"S1471068421000600_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.03.001"},{"key":"S1471068421000600_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/289121.289130"},{"key":"S1471068421000600_ref52","volume-title":"Partial Evaluation and Automatic Program Generation","author":"Jones","year":"1993"},{"key":"S1471068421000600_ref5","first-page":"1","article-title":"A Practical Partial Evaluation Scheme for Multi-Paradigm Declarative Languages","volume":"2002","author":"Albert","year":"2002","journal-title":"Journal of Functional and Logic Programming"},{"key":"S1471068421000600_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/258993.259015"},{"key":"S1471068421000600_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-021-09771-1"},{"key":"S1471068421000600_ref27","unstructured":"Bae, K. , Escobar, S. , and Meseguer, J. (2013). Abstract Logical Model Checking of Infinite-State Systems Using Narrowing. In Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013), volume 21 of Leibniz International Proceedings in Informatics (LIPIcs), pages 81\u201396. Schloss Dagstuhl - Leibniz-Zentrum f\u00dcr Informatik."},{"key":"S1471068421000600_ref2","unstructured":"Albert, E. , Alpuente, M. , Falaschi, M. , and Vidal, G. (1998). Indy User\u2019s Manual. Technical Report DSIC-II\/12\/98, Department of Computer Systems and Computation, Universitat Polit\u00e8cnica de Val\u00e8ncia."},{"key":"S1471068421000600_ref7","volume-title":"Festschrift volume in honor of Manuel Hermenegildo (submitted, invited contribution)","author":"Alpuente","year":"2021"},{"key":"S1471068421000600_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.07.013"},{"key":"S1471068421000600_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.02.006"},{"key":"S1471068421000600_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58156-1_15"},{"key":"S1471068421000600_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.05.012"},{"key":"S1471068421000600_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_27"},{"key":"S1471068421000600_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"S1471068421000600_ref47","unstructured":"Gallagher, J. P. and Bruynooghe, M. (1990). The Derivation of an Algorithm for Program Specialisation. In Proceedings of the 7th International Conference on Logic Programming (ICLP 1990), pages 732\u2013746. The MIT Press."},{"key":"S1471068421000600_ref59","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.06.001"},{"key":"S1471068421000600_ref63","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"S1471068421000600_ref75","first-page":"1","article-title":"Executing Multilevel Domain-Specific Models in Maude","volume":"18","author":"Rodrguez","year":"2019","journal-title":"Journal of Object Technology"},{"key":"S1471068421000600_ref55","doi-asserted-by":"publisher","DOI":"10.1145\/1111542.1111557"},{"key":"S1471068421000600_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321996"},{"key":"S1471068421000600_ref26","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068404002303"},{"key":"S1471068421000600_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"S1471068421000600_ref62","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(95)00095-X"},{"key":"S1471068421000600_ref70","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9000-6"},{"key":"S1471068421000600_ref66","doi-asserted-by":"crossref","unstructured":"Meseguer, J. (2015). Variant-Based Satisfiability in Initial Algebras. In Proceedings of the 4th International Workshop for Safety-Critical Systems (FTSCS 2015), volume 596 of Communications in Computer and Information Science, pages 3\u201334. Springer.","DOI":"10.1007\/978-3-319-29510-7_1"},{"key":"S1471068421000600_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(99)00030-8"},{"key":"S1471068421000600_ref61","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00357-7"},{"key":"S1471068421000600_ref64","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"S1471068421000600_ref74","unstructured":"Rosu, G. (2017). K: A Semantic Framework for Programming Languages and Formal Analysis Tools. In Dependable Software Systems Engineering, volume 50 of NATO Science for Peace and Security Series - D: Information and Communication Security, pages 186\u2013206. IOS Press."},{"key":"S1471068421000600_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48242-3_23"},{"key":"S1471068421000600_ref9","first-page":"124","article-title":"Optimization of Rewrite Theories by Equational Partial Evaluation","author":"Alpuente","year":"2022","journal-title":"Journal of Logical and Algebraic Methods in Programming"},{"key":"S1471068421000600_ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54624-2_16"},{"key":"S1471068421000600_ref60","doi-asserted-by":"crossref","unstructured":"Martens, B. and Gallagher, J. P. (1995). Ensuring Global Termination of Partial Deduction while Allowing Flexible Polyvariance. In Proceedings of the 12th International Conference on Logic Programming (ICLP 1995), pages 597\u2013611. The MIT Press.","DOI":"10.7551\/mitpress\/4298.003.0059"},{"key":"S1471068421000600_ref65","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013826"},{"key":"S1471068421000600_ref73","first-page":"153","article-title":"A Note on Inductive Generalization","volume":"5","author":"Plotkin","year":"1970","journal-title":"Machine Intelligence"},{"key":"S1471068421000600_ref38","first-page":"110","article-title":"Programming and Symbolic Computation in Maude","author":"Dur\u00e1n","year":"2020","journal-title":"Journal of Logical and Algebraic Methods in Programming"},{"key":"S1471068421000600_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12904-4_4"},{"key":"S1471068421000600_ref49","doi-asserted-by":"crossref","unstructured":"Hanus, M. (1994). The Integration of Functions into Logic Programming: From Theory to Practice. The Journal of Logic Programming, 19\/20:583\u2013628.","DOI":"10.1016\/0743-1066(94)90034-5"}],"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\/S1471068421000600","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,18]],"date-time":"2024-09-18T10:04:21Z","timestamp":1726653861000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068421000600\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,2,11]]},"references-count":79,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,5]]}},"alternative-id":["S1471068421000600"],"URL":"https:\/\/doi.org\/10.1017\/s1471068421000600","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,2,11]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}