{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T01:30:31Z","timestamp":1785202231191,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,10,18]],"date-time":"2023-10-18T00:00:00Z","timestamp":1697587200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003359","name":"Generalitat Valenciana","doi-asserted-by":"publisher","award":["CIPROM\/2022\/6"],"award-info":[{"award-number":["CIPROM\/2022\/6"]}],"id":[{"id":"10.13039\/501100003359","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100014440","name":"Ministerio de Ciencia, Innovaci\u00f3n y Universidades","doi-asserted-by":"publisher","award":["PID2021-122830OB-C42"],"award-info":[{"award-number":["PID2021-122830OB-C42"]}],"id":[{"id":"10.13039\/100014440","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"publisher","award":["EC H2020- EU grant agreement No. 952215 (TAILOR)"],"award-info":[{"award-number":["EC H2020- EU grant agreement No. 952215 (TAILOR)"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100014440","name":"Ministerio de Ciencia, Innovaci\u00f3n y Universidades","doi-asserted-by":"publisher","award":["PCI2020-120708-2"],"award-info":[{"award-number":["PCI2020-120708-2"]}],"id":[{"id":"10.13039\/100014440","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004233","name":"Universitat Polit\u00e8cnica de Val\u00e8ncia","doi-asserted-by":"publisher","award":["FPI-2022-S2-49802"],"award-info":[{"award-number":["FPI-2022-S2-49802"]}],"id":[{"id":"10.13039\/501100004233","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,10,18]]},"DOI":"10.1145\/3623503.3623537","type":"proceedings-article","created":{"date-parts":[[2023,10,19]],"date-time":"2023-10-19T14:34:51Z","timestamp":1697726091000},"page":"14-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Symbolic Analysis by Using Folding Narrowing with Irreducibility and SMT Constraints"],"prefix":"10.1145","author":[{"given":"Santiago","family":"Escobar","sequence":"first","affiliation":[{"name":"Universitat Polit\u00e8cnica de Val\u00e8ncia, Valencia, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ra\u00fal","family":"L\u00f3pez-Rueda","sequence":"additional","affiliation":[{"name":"Universitat Polit\u00e8cnica de Val\u00e8ncia, Valencia, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Julia","family":"Sapi\u00f1a","sequence":"additional","affiliation":[{"name":"Universitat Polit\u00e8cnica de Val\u00e8ncia, Valencia, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,10,19]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/167088.167242"},{"key":"e_1_3_2_1_2_1","volume-title":"IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability","author":"Andr\u00e9 \u00c9tienne","unstructured":"\u00c9tienne Andr\u00e9 . 2021. IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability . In Computer Aided Verification, Alexandra Silva and K. Rustan M. Leino (Eds.). Springer International Publishing , Cham . 552\u2013565. isbn:978-3-030-81685-8 \u00c9tienne Andr\u00e9. 2021. IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability. In Computer Aided Verification, Alexandra Silva and K. Rustan M. Leino (Eds.). Springer International Publishing, Cham. 552\u2013565. isbn:978-3-030-81685-8"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563822.3569923"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.RTA.2013.81"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.RTA.2013.81"},{"key":"e_1_3_2_1_6_1","unstructured":"M. Clavel F. Dur\u00e1n S. Eker S. Escobar P. Lincoln N. Mart\u00ed-Oliet J. Meseguer R. Rubio and C. Talcott. 2022. Maude Manual (Version 3.2.1). SRI International Computer Science Laboratory. Available at: http:\/\/maude.cs.illinois.edu \t\t\t\t  M. Clavel F. Dur\u00e1n S. Eker S. Escobar P. Lincoln N. Mart\u00ed-Oliet J. Meseguer R. Rubio and C. Talcott. 2022. Maude Manual (Version 3.2.1). SRI International Computer Science Laboratory. Available at: http:\/\/maude.cs.illinois.edu"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_22"},{"key":"e_1_3_2_1_8_1","volume-title":"Z3: an efficient SMT solver. In 2008 Tools and Algorithms for Construction and Analysis of Systems","author":"de Moura Leonardo","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner . 2008. Z3: an efficient SMT solver. In 2008 Tools and Algorithms for Construction and Analysis of Systems . Springer , Berlin, Heidelberg , 337\u2013340. https:\/\/www.microsoft.com\/en-us\/research\/publication\/z3-an-efficient-smt-solver\/ Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: an efficient SMT solver. In 2008 Tools and Algorithms for Construction and Analysis of Systems. Springer, Berlin, Heidelberg, 337\u2013340. https:\/\/www.microsoft.com\/en-us\/research\/publication\/z3-an-efficient-smt-solver\/"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-10769-6_31"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.RTA.2011.31"},{"key":"e_1_3_2_1_11_1","volume-title":"Computer Aided Verification","author":"Dutertre Bruno","unstructured":"Bruno Dutertre . 2014. Yices 2.2. In Computer Aided Verification , Armin Biere and Roderick Bloem (Eds.). Springer International Publishing , Cham . 737\u2013744. isbn:978-3-319-08867-9 Bruno Dutertre. 2014. Yices 2.2. In Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham. 737\u2013744. isbn:978-3-319-08867-9"},{"key":"e_1_3_2_1_12_1","volume-title":"Proceedings of the 17th European Symposium on Research in Computer Security (ESORICS 2012)","volume":"90","author":"Erbatur S.","unstructured":"S. Erbatur , S. Escobar , D. Kapur , Z. Liu , C. Lynch , C. Meadows , J. Meseguer , P. Narendran , S. Santiago , and R. Sasse . 2012. Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions . In Proceedings of the 17th European Symposium on Research in Computer Security (ESORICS 2012) (Lecture Notes in Computer Science , Vol. 7459). Springer, 73\u2013 90 . S. Erbatur, S. Escobar, D. Kapur, Z. Liu, C. Lynch, C. Meadows, J. Meseguer, P. Narendran, S. Santiago, and R. Sasse. 2012. Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions. In Proceedings of the 17th European Symposium on Research in Computer Security (ESORICS 2012) (Lecture Notes in Computer Science, Vol. 7459). Springer, 73\u201390."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73449-9_13"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-19052-1_4"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.01.002"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/947864.947865"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1137\/0215084"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563822.3568016"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_2"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-12441-9_3"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-12441-9_8"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","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. arxiv:2307.06348. \t\t\t\t  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. arxiv:2307.06348.","DOI":"10.1016\/j.jlamp.2023.100895"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2023.100895"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-64299-4_26"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.12.026"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.100483"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-68446-4_1"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9000-6"},{"key":"e_1_3_2_1_31_1","volume-title":"Computer Algebra in Scientific Computing, Vladimir P","author":"Monniaux David","unstructured":"David Monniaux . 2016. A Survey of Satisfiability Modulo Theory . In Computer Algebra in Scientific Computing, Vladimir P . Gerdt, Wolfram Koepf, Werner M. Seiler, and Evgenii V. Vorozhtsov (Eds.). Springer International Publishing , Cham . 401\u2013425. isbn:978-3-319-45641-6 David Monniaux. 2016. A Survey of Satisfiability Modulo Theory. In Computer Algebra in Scientific Computing, Vladimir P. Gerdt, Wolfram Koepf, Werner M. Seiler, and Evgenii V. Vorozhtsov (Eds.). Springer International Publishing, Cham. 401\u2013425. isbn:978-3-319-45641-6"},{"key":"e_1_3_2_1_32_1","volume-title":"The Real-Time Maude Tool. In Proceedings of the 14th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2008)","volume":"336","author":"\u00d6lveczky P. C.","unstructured":"P. C. \u00d6lveczky and J. Meseguer . 2008 . The Real-Time Maude Tool. In Proceedings of the 14th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2008) (Lecture Notes in Computer Science , Vol. 4963). Springer, 332\u2013 336 . P. C. \u00d6lveczky and J. Meseguer. 2008. The Real-Time Maude Tool. In Proceedings of the 14th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2008) (Lecture Notes in Computer Science, Vol. 4963). Springer, 332\u2013336."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.10.001"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680400526X"}],"event":{"name":"FTSCS '23: 9th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems","location":"Cascais Portugal","acronym":"FTSCS '23","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGAda ACM Special Interest Group on Ada Programming Language"]},"container-title":["Proceedings of the 9th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3623503.3623537","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3623503.3623537","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:51:01Z","timestamp":1750287061000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3623503.3623537"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,18]]},"references-count":34,"alternative-id":["10.1145\/3623503.3623537","10.1145\/3623503"],"URL":"https:\/\/doi.org\/10.1145\/3623503.3623537","relation":{},"subject":[],"published":{"date-parts":[[2023,10,18]]},"assertion":[{"value":"2023-10-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}