{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:22:16Z","timestamp":1765617736748,"version":"3.48.0"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","funder":[{"name":"Generalitat Valenciana","award":["CIPROM\/2022\/6"],"award-info":[{"award-number":["CIPROM\/2022\/6"]}]},{"name":"INCIBE's Chair funded by the EU-NextGenerationEU through the Spanish government's Plan de Recuperaci\u00f3n, Transformaci\u00f3n y Resiliencia","award":["Chair Program"],"award-info":[{"award-number":["Chair Program"]}]},{"name":"MCIN\/AEI\/10.13039\/501100011033 and ERDF A way of making Europe","award":["PID2021-122830OB-C42"],"award-info":[{"award-number":["PID2021-122830OB-C42"]}]},{"name":"NATO Science for Peace and Security Programme","award":["G6133"],"award-info":[{"award-number":["G6133"]}]},{"name":"JSPS KAKENHI","award":["JP23K28060"],"award-info":[{"award-number":["JP23K28060"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,9,10]]},"DOI":"10.1145\/3756907.3756911","type":"proceedings-article","created":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:19:11Z","timestamp":1765617551000},"page":"1-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Folding Narrowing for the Analysis of Mutual Exclusion Protocols"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2550-8041","authenticated-orcid":false,"given":"Ra\u00fal","family":"L\u00f3pez-Rueda","sequence":"first","affiliation":[{"name":"Universitat Polit\u00e8cnica de Val\u00e8ncia, Val\u00e8ncia, Val\u00e8ncia, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7092-2084","authenticated-orcid":false,"given":"Duong Dinh","family":"Tran","sequence":"additional","affiliation":[{"name":"Japan Advanced Institute of Science and Technology, Nomi, Ishikawa, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1601-4584","authenticated-orcid":false,"given":"Canh Minh","family":"Do","sequence":"additional","affiliation":[{"name":"Japan Advanced Institute of Science and Technology, Nomi, Ishikawa, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3550-4781","authenticated-orcid":false,"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[{"name":"Universitat Polit\u00e8cnica de Val\u00e8ncia, Val\u00e8ncia, Val\u00e8ncia, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4441-3259","authenticated-orcid":false,"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[{"name":"Japan Advanced Institute of Science and Technology, Nomi, Ishikawa, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,12,13]]},"reference":[{"key":"e_1_3_3_1_2_2","doi-asserted-by":"publisher","unstructured":"Thomas\u00a0E. Anderson. 1990. The Performance of Spin Lock Alternatives for Shared-Memory Multiprocessors. IEEE Trans. Parallel Distributed Syst. 1 1 (1990) 6\u201316. 10.1109\/71.80120","DOI":"10.1109\/71.80120"},{"key":"e_1_3_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65941-6_1"},{"key":"e_1_3_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.RTA.2013.81"},{"key":"e_1_3_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08918-8_5"},{"key":"e_1_3_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_22"},{"key":"e_1_3_3_1_7_2","doi-asserted-by":"publisher","unstructured":"Rohit Chadha Vincent Cheval \u015etefan Ciob\u00e2c\u0103 and Steve Kremer. 2016. Automated Verification of Equivalence Properties of Cryptographic Protocols. ACM Trans. Comput. Log. 17 4 (2016) 23. 10.1145\/2926715","DOI":"10.1145\/2926715"},{"key":"e_1_3_3_1_8_2","volume-title":"Maude Manual (Version 3.5.1)","author":"Clavel M.","year":"2025","unstructured":"M. Clavel, F. Dur\u00e1n, S. Eker, S. Escobar, P. Lincoln, N. Mart\u00ed-Oliet, J. Meseguer, R. Rubio, and C. Talcott. 2025. Maude Manual (Version 3.5.1). Technical Report. SRI International Computer Science Laboratory. Available at: http:\/\/maude.cs.illinois.edu."},{"key":"e_1_3_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1"},{"key":"e_1_3_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_22"},{"key":"e_1_3_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1142\/3831"},{"key":"e_1_3_3_1_12_2","doi-asserted-by":"publisher","unstructured":"E.\u00a0W. Dijkstra. 1965. Solution of a problem in concurrent programming control. Commun. ACM 8 9 (Sept. 1965) 569. 10.1145\/365559.365617","DOI":"10.1145\/365559.365617"},{"key":"e_1_3_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3678232.3678236"},{"key":"e_1_3_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54624-2_16"},{"key":"e_1_3_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99840-4_2"},{"key":"e_1_3_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-71"},{"key":"e_1_3_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73449-9_13"},{"key":"e_1_3_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-19052-1_4"},{"key":"e_1_3_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2009.05.015"},{"key":"e_1_3_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2007.01.004"},{"key":"e_1_3_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16310-4_5"},{"key":"e_1_3_3_1_22_2","doi-asserted-by":"publisher","unstructured":"Santiago Escobar Ralf Sasse and Jos\u00e9 Meseguer. 2012. Folding variant narrowing and optimal variant termination. J. Log. Algebraic Methods Program. 81 7-8 (2012) 898\u2013928. 10.1016\/J.JLAP.2012.01.002","DOI":"10.1016\/J.JLAP.2012.01.002"},{"key":"e_1_3_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.5555\/2385452"},{"key":"e_1_3_3_1_24_2","doi-asserted-by":"crossref","unstructured":"Jean-Pierre Jouannaud and H\u00e9l\u00e8ne Kirchner. 1986. Completion of a Set of Rules Modulo a Set of Equations. SIAM J. Comput. 15 4 (1986) 1155\u20131194.","DOI":"10.1137\/0215084"},{"key":"e_1_3_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_2"},{"key":"e_1_3_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-12441-9_8"},{"key":"e_1_3_3_1_27_2","doi-asserted-by":"publisher","unstructured":"Ra\u00fal L\u00f3pez-Rueda Santiago Escobar and Julia Sapi\u00f1a. 2023. An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis. J. Log. Algebraic Methods Program. 135 (2023) 100895. 10.1016\/J.JLAMP.2023.100895","DOI":"10.1016\/J.JLAMP.2023.100895"},{"key":"e_1_3_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"e_1_3_3_1_29_2","doi-asserted-by":"publisher","unstructured":"Jos\u00e9 Meseguer. 1992. Conditioned Rewriting Logic as a United Model of Concurrency. Theor. Comput. Sci. 96 1 (1992) 73\u2013155. 10.1016\/0304-3975(92)90182-F","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"e_1_3_3_1_30_2","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Recent Trends in Algebraic Development Techniques","author":"Meseguer Jos\u00e9","year":"1998","unstructured":"Jos\u00e9 Meseguer. 1998. Membership algebra as a logical framework for equational specification. In Recent Trends in Algebraic Development Techniques, Francesco\u00a0Parisi Presicce (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 18\u201361."},{"key":"e_1_3_3_1_31_2","doi-asserted-by":"publisher","unstructured":"Jos\u00e9 Meseguer. 2017. Strict coherence of conditional rewriting modulo axioms. Theor. Comput. Sci. 672 (2017) 1\u201335. 10.1016\/j.tcs.2016.12.026","DOI":"10.1016\/j.tcs.2016.12.026"},{"key":"e_1_3_3_1_32_2","doi-asserted-by":"crossref","unstructured":"Jos\u00e9 Meseguer and Prasanna Thati. 2007. Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Higher-Order and Symbolic Computation 20 1-2 (2007) 123\u2013160.","DOI":"10.1007\/s10990-007-9000-6"},{"key":"e_1_3_3_1_33_2","doi-asserted-by":"publisher","unstructured":"Kazuhiro Ogata and Kokichi Futatsugi. 2013. Compositionally Writing Proof Scores of Invariants in the OTS\/CafeOBJ Method. J. Univers. Comput. Sci. 19 6 (2013) 771\u2013804. 10.3217\/JUCS-019-06-0771","DOI":"10.3217\/JUCS-019-06-0771"},{"key":"e_1_3_3_1_34_2","doi-asserted-by":"publisher","unstructured":"Adri\u00e1n Riesco and Kazuhiro Ogata. 2018. Prove it! Inferring Formal Proof Scripts from CafeOBJ Proof Scores. ACM Trans. Softw. Eng. Methodol. 27 2 (2018) 6:1\u20136:32. 10.1145\/3208951","DOI":"10.1145\/3208951"},{"key":"e_1_3_3_1_35_2","volume-title":"Term Rewriting Systems","year":"2003","unstructured":"TeReSe (Ed.). 2003. Term Rewriting Systems. Cambridge University Press, Cambridge."},{"key":"e_1_3_3_1_36_2","doi-asserted-by":"publisher","unstructured":"Duong\u00a0Dinh Tran Dang\u00a0Duy Bui and Kazuhiro Ogata. 2021. Simulation-Based Invariant Verification Technique for the OTS\/CafeOBJ Method. IEEE Access 9 (2021) 93847\u201393870. 10.1109\/ACCESS.2021.3093211","DOI":"10.1109\/ACCESS.2021.3093211"},{"key":"e_1_3_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.18293\/SEKE2020-064"},{"key":"e_1_3_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC54236.2022.00164"}],"event":{"name":"PPDP '25: Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming","location":"Rende Italy","acronym":"PPDP '25"},"container-title":["Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3756907.3756911","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:19:36Z","timestamp":1765617576000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3756907.3756911"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,10]]},"references-count":37,"alternative-id":["10.1145\/3756907.3756911","10.1145\/3756907"],"URL":"https:\/\/doi.org\/10.1145\/3756907.3756911","relation":{},"subject":[],"published":{"date-parts":[[2025,9,10]]},"assertion":[{"value":"2025-12-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}