{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T07:54:00Z","timestamp":1791446040980,"version":"4.3.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032048479","type":"print"},{"value":"9783032048486","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T00:00:00Z","timestamp":1757376000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T00:00:00Z","timestamp":1757376000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-04848-6_1","type":"book-chapter","created":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T11:58:57Z","timestamp":1757678337000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Symbolic Computation and\u00a0Verification Methods in\u00a0Maude"],"prefix":"10.1007","author":[{"given":"Jos\u00e9","family":"Meseguer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,9,9]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Agha, G.: Actors. MIT Press, Cambridge (1986)","DOI":"10.7551\/mitpress\/1086.001.0001"},{"issue":"3\u20134","key":"1_CR2","doi-asserted-by":"publisher","first-page":"297","DOI":"10.3233\/FI-2020-1991","volume":"177","author":"M Alpuente","year":"2020","unstructured":"Alpuente, M., Cuenca-Ortega, A., Escobar, S., Meseguer, J.: Order-sorted homeomorphic embedding modulo combinations of associativity and\/or commutativity axioms. Fundam. Informaticae 177(3\u20134), 297\u2013329 (2020)","journal-title":"Fundam. Informaticae"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Alpuente, M., Cuenca-Ortega, A., Escobar, S., Meseguer, J.: A partial evaluation framework for order-sorted equational programs modulo axioms. J. Log. Algebraic Methods Program. 110 (2020)","DOI":"10.1016\/j.jlamp.2019.100501"},{"key":"1_CR4","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1016\/j.ic.2014.01.006","volume":"235","author":"M Alpuente","year":"2014","unstructured":"Alpuente, M., Escobar, S., Espert, J., Meseguer, J.: A modular order-sorted equational generalization algorithm. Inf. Comput. 235, 98\u2013136 (2014)","journal-title":"Inf. Comput."},{"issue":"5","key":"1_CR5","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/s10472-021-09771-1","volume":"90","author":"M Alpuente","year":"2022","unstructured":"Alpuente, M., Escobar, S., Meseguer, J., Sapi\u00f1a, J.: Order-sorted equational generalization algorithm revisited. Ann. Math. Artif. Intell. 90(5), 499\u2013522 (2022)","journal-title":"Ann. Math. Artif. Intell."},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Bae, K., Escobar, S., L\u00f3pez-Rueda, R., Meseguer, J., Sapi\u00f1a, J.: Verifying invariants by deductive model checking. In: Rewriting Logic and Its Applications \u2013 WRLA 2024. Lecture Notes in Computer Science, vol. 14953, pp. 3\u201321. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-65941-6_1"},{"key":"1_CR7","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: Rewriting Techniques and Applications (RTA 2013). LIPIcs, vol.\u00a021, pp. 81\u201396. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik (2013)"},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1016\/j.scico.2014.02.006","volume":"99","author":"K Bae","year":"2015","unstructured":"Bae, K., Meseguer, J.: Model checking linear temporal logic of rewriting formulas under localized fairness. Sci. Comput. Program. 99, 193\u2013234 (2015)","journal-title":"Sci. Comput. Program."},{"key":"1_CR9","unstructured":"van Benthem, J.: Modal Logic for Open Minds. Center for the Study of Language and Information. Stanford University (2010)"},{"key":"1_CR10","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1016\/j.scico.2015.06.001","volume":"112","author":"A Cholewa","year":"2015","unstructured":"Cholewa, A., Escobar, S., Meseguer, J.: Constrained narrowing for conditional equational theories modulo axioms. Sci. Comput. Program. 112, 24\u201357 (2015)","journal-title":"Sci. Comput. Program."},{"key":"1_CR11","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)"},{"key":"1_CR12","unstructured":"Clavel, M., et al.: All About Maude \u2013 A High-Performance Logical Framework. Springer LNCS, vol. 4350 (2007)"},{"key":"1_CR13","unstructured":"Clavel, M., et al.: Maude Manual (Version 3.1) (2020). http:\/\/maude.cs.uiuc.edu"},{"key":"1_CR14","unstructured":"Clavel, M., et al.: Maude Manual (Version 3.5.1) (2025). https:\/\/maude.cs.illinois.edu\/manual.pdf"},{"key":"1_CR15","unstructured":"CVC4: https:\/\/cvc4.github.io"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., et al.: Programming and symbolic computation in Maude. J. Log. Algebraic Methods Program. 110 (2020)","DOI":"10.1016\/j.jlamp.2019.100497"},{"key":"1_CR17","doi-asserted-by":"publisher","first-page":"816","DOI":"10.1016\/j.jlap.2011.12.004","volume":"81","author":"F Dur\u00e1n","year":"2012","unstructured":"Dur\u00e1n, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Algebraic Logic Program. 81, 816\u2013850 (2012)","journal-title":"J. Algebraic Logic Program."},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F.J., Escobar, S., Meseguer, J., Sapi\u00f1a, J.: NuITP: an inductive theorem prover for equational program verification. In: Bruni, A., Momigliano, A., Pradella, M., Rossi, M., Cheney, J. (eds.) Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming, PPDP 2024, Milano, Italy, September 9-11, 2024, pp. 6:1\u20136:11. ACM (2024). https:\/\/doi.org\/10.1145\/3678232.3678236","DOI":"10.1145\/3678232.3678236"},{"key":"1_CR19","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2021.100747","volume":"126","author":"S Eker","year":"2022","unstructured":"Eker, S.: Associative unification in Maude. J. Logical Algebraic Methods Program. 126, 100747 (2022)","journal-title":"J. Logical Algebraic Methods Program."},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03829-7_1","volume-title":"Foundations of Security Analysis and Design V","author":"S Escobar","year":"2009","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 1\u201350. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03829-7_1"},{"key":"1_CR21","doi-asserted-by":"publisher","first-page":"898","DOI":"10.1016\/j.jlap.2012.01.002","volume":"81","author":"S Escobar","year":"2012","unstructured":"Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Algebraic Logic Program. 81, 898\u2013928 (2012)","journal-title":"J. Algebraic Logic Program."},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/3-540-10009-1_25","volume-title":"5th Conference on Automated Deduction Les Arcs, France, July 8\u201311, 1980","author":"J-M Hullot","year":"1980","unstructured":"Hullot, J.-M.: Canonical forms and unification. In: Bibel, W., Kowalski, R. (eds.) CADE 1980. LNCS, vol. 87, pp. 318\u2013334. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10009-1_25"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0036921","volume-title":"Automata, Languages and Programming","author":"J-P Jouannaud","year":"1983","unstructured":"Jouannaud, J.-P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: Diaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 361\u2013373. Springer, Heidelberg (1983). https:\/\/doi.org\/10.1007\/BFb0036921"},{"key":"1_CR24","unstructured":"Lankford, D.S.: Canonical inference. Technical report ATP-32, Southwestn Univ. (1975)"},{"key":"1_CR25","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2023.100895","volume":"135","author":"R L\u00f3pez-Rueda","year":"2023","unstructured":"L\u00f3pez-Rueda, R., Escobar, S., Sapi\u00f1a, J.: An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis. J. Log. Algebraic Methods Program. 135, 100895 (2023)","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"1\u20132","key":"1_CR26","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10990-007-9000-6","volume":"20","author":"J Meseguer","year":"2007","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols. J. Higher-Order Symbolic Comput. 20(1\u20132), 123\u2013160 (2007)","journal-title":"J. Higher-Order Symbolic Comput."},{"issue":"1","key":"1_CR27","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: A logical theory of concurrent objects and its realization in the Maude language. In: Agha, G., Wegner, P., Yonezawa, A. (eds.) Research Directions in Concurrent Object-Oriented Programming, pp. 314\u2013390. MIT Press (1993)","DOI":"10.7551\/mitpress\/2087.003.0017"},{"key":"1_CR29","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Algebraic Logic Program. 81, 721\u2013781 (2012)","journal-title":"J. Algebraic Logic Program."},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-662-49630-5_29","volume-title":"Foundations of Software Science and Computation Structures","author":"J Meseguer","year":"2016","unstructured":"Meseguer, J.: Order-sorted rewriting and congruence closure. In: Jacobs, B., L\u00f6ding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 493\u2013509. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49630-5_29"},{"key":"1_CR31","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2017.09.001","volume":"154","author":"J Meseguer","year":"2018","unstructured":"Meseguer, J.: Variant-based satisfiability in initial algebras. Sci. Comput. Program. 154, 3\u201341 (2018)","journal-title":"Sci. Comput. Program."},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Generalized rewrite theories, coherence completion, and symbolic methods. J. Log. Algebraic Methods Program. 110 (2020)","DOI":"10.1016\/j.jlamp.2019.100483"},{"key":"1_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-68446-4_1","volume-title":"Logic-Based Program Synthesis and Transformation","author":"J Meseguer","year":"2021","unstructured":"Meseguer, J.: Symbolic computation in Maude: some tapas. In: LOPSTR 2020. LNCS, vol. 12561, pp. 3\u201336. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-68446-4_1"},{"key":"1_CR34","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2023.100877","volume":"134","author":"J Meseguer","year":"2023","unstructured":"Meseguer, J.: Variants and satisfiability in the infinitary unification wonderland. J. Log. Algebraic Methods Program. 134, 100877 (2023)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"1_CR35","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2025.101036","volume":"144","author":"J Meseguer","year":"2025","unstructured":"Meseguer, J.: Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification. J. Log. Algebraic Methods Program. 144, 101036 (2025)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"1_CR36","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/j.jlamp.2016.10.001","volume":"86","author":"C Rocha","year":"2017","unstructured":"Rocha, C., Meseguer, J., Mu\u00f1oz, C.A.: Rewriting modulo SMT and open system analysis. J. Logic Algebraic Methods Program. 86, 269\u2013297 (2017)","journal-title":"J. Logic Algebraic Methods Program."},{"issue":"4","key":"1_CR37","doi-asserted-by":"publisher","first-page":"315","DOI":"10.3233\/FI-2020-1926","volume":"173","author":"S Skeirik","year":"2020","unstructured":"Skeirik, S., Stefanescu, A., Meseguer, J.: A constructor-based reachability logic for rewrite theories. Fundam. Inform. 173(4), 315\u2013382 (2020)","journal-title":"Fundam. Inform."},{"issue":"4","key":"1_CR38","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"JR Slagle","year":"1974","unstructured":"Slagle, J.R.: Automated theorem-proving for theories with simplifiers commutativity, and associativity. J. ACM 21(4), 622\u2013642 (1974)","journal-title":"J. ACM"},{"key":"1_CR39","unstructured":"Yices. https:\/\/yices.csl.sri.com"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-04848-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T07:07:18Z","timestamp":1791443238000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04848-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,9]]},"ISBN":["9783032048479","9783032048486"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04848-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,9]]},"assertion":[{"value":"9 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The author has no competing interests to declare that\u00a0are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"LOPSTR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Logic-Based Program Synthesis and Transformation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rende","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lopstr2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/lopstr.github.io\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}