{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T23:46:47Z","timestamp":1740181607481,"version":"3.37.3"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"8","license":[{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"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":["SN COMPUT. SCI."],"DOI":"10.1007\/s42979-024-03371-6","type":"journal-article","created":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T16:15:40Z","timestamp":1731946540000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["CHC-Based Verification of Programs Through Graph Decompositions"],"prefix":"10.1007","volume":"5","author":[{"given":"Marco","family":"Faella","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8697-2980","authenticated-orcid":false,"given":"Giulio","family":"Garbi","sequence":"additional","affiliation":[]},{"given":"Salvatore","family":"La Torre","sequence":"additional","affiliation":[]},{"given":"Gennaro","family":"Parlato","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,18]]},"reference":[{"key":"3371_CR1","doi-asserted-by":"publisher","unstructured":"Alur R, Madhusudan P. Adding nesting structure to words. In: Ibarra, OH, Dang Z, editors. Developments in language theory, 10th international conference, DLT 2006, Santa Barbara, CA, USA, June 26\u201329, 2006. Proceedings, vol. 4036. Lecture notes in computer science. Springer; 2006. pp. 1\u201313. https:\/\/doi.org\/10.1007\/11779148_1 .","DOI":"10.1007\/11779148_1"},{"key":"3371_CR2","doi-asserted-by":"publisher","unstructured":"Madhusudan P, Parlato G. The tree width of auxiliary storage. In: Ball T, Sagiv M, editors. Proceedings of the 38th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2011, Austin, TX, USA, 26\u201328, 2011. ACM; 2011. pp. 283\u2013294. https:\/\/doi.org\/10.1145\/1926385.1926419.","DOI":"10.1145\/1926385.1926419"},{"key":"3371_CR3","doi-asserted-by":"publisher","unstructured":"Faella M, Parlato G. Reasoning about data trees using CHCs. In: Shoham S, Vizel Y, editors. Computer aided verification\u201434th international conference, CAV 2022, Haifa, Israel, August 7\u201310, 2022, proceedings, part II, vol. 13372. Lecture notes in computer science. Springer; 2022. pp. 249\u2013271. https:\/\/doi.org\/10.1007\/978-3-031-13188-2_13.","DOI":"10.1007\/978-3-031-13188-2_13"},{"key":"3371_CR4","doi-asserted-by":"publisher","unstructured":"Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A. Synthesizing software verifiers from proof rules. In: Vitek J, Lin H, Tip F, editors. ACM SIGPLAN conference on programming language design and implementation, PLDI \u201912, Beijing, China\u2014June 11\u201316, 2012. ACM; 2012. pp. 405\u2013416. https:\/\/doi.org\/10.1145\/2254064.2254112.","DOI":"10.1145\/2254064.2254112"},{"key":"3371_CR5","doi-asserted-by":"publisher","unstructured":"Gurfinkel A, Bj\u00f8rner N. The science, art, and magic of constrained Horn clauses. In: 21st International symposium on symbolic and numeric algorithms for scientific computing, SYNASC 2019, Timisoara, Romania, September 4\u20137 , 2019. IEEE; 2019. pp. 6\u201310. https:\/\/doi.org\/10.1109\/SYNASC49474.2019.00010.","DOI":"10.1109\/SYNASC49474.2019.00010"},{"key":"3371_CR6","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner N, Gurfinkel A, McMillan KL, Rybalchenko A. Horn clause solvers for program verification. In: Beklemishev LD, Blass A, Dershowitz N, Finkbeiner B, Schulte W, editors. Fields of logic and computation II\u2014Essays dedicated to Yuri Gurevich on the occasion of his 75th birthday, vol. 9300. Lecture notes in computer science. Springer; 2015. pp. 24\u201351. https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2.","DOI":"10.1007\/978-3-319-23534-9_2"},{"issue":"7","key":"3371_CR7","doi-asserted-by":"publisher","first-page":"1393","DOI":"10.1007\/s10817-020-09571-y","volume":"64","author":"A Champion","year":"2020","unstructured":"Champion A, Chiba T, Kobayashi N, Sato R. Ice-based refinement type discovery for higher-order functional programs. J Autom Reason. 2020;64(7):1393\u2013418. https:\/\/doi.org\/10.1007\/s10817-020-09571-y.","journal-title":"J Autom Reason"},{"key":"3371_CR8","doi-asserted-by":"publisher","unstructured":"Fedyukovich G, Ahmad MBS, Bod\u00edk R. Gradual synthesis for static parallelization of single-pass array-processing programs. In: Cohen A, Vechev MT, editors. Proceedings of the 38th ACM SIGPLAN conference on programming language design and implementation, PLDI 2017, Barcelona, Spain, June 18\u201323, 2017. ACM; pp. 572\u2013585. https:\/\/doi.org\/10.1145\/3062341.3062382.","DOI":"10.1145\/3062341.3062382"},{"key":"3371_CR9","doi-asserted-by":"publisher","unstructured":"Garoche P, Kahsai T, Thirioux X. Hierarchical state machines as modular Horn clauses. In: Gallagher JP, R\u00fcmmer P, editors. Proceedings 3rd workshop on horn clauses for verification and synthesis, HCVS@ETAPS 2016, vol. 219. Eindhoven, The Netherlands, 3rd April 2016. EPTCS; 2016. pp. 15\u201328. https:\/\/doi.org\/10.4204\/EPTCS.219.2.","DOI":"10.4204\/EPTCS.219.2"},{"key":"3371_CR10","doi-asserted-by":"publisher","unstructured":"Gurfinkel A, Kahsai T, Komuravelli A, Navas JA. The seahorn verification framework. In: Kroening D, Pasareanu CS, editors. Computer aided verification\u201427th international conference, CAV 2015, San Francisco, CA, USA, July 18\u201324, 2015, proceedings, part I, vol. 9206. Lecture notes in computer science. Springer; 2015. pp. 343\u2013361. https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20.","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"3371_CR11","doi-asserted-by":"publisher","unstructured":"Hojjat H, Konecn\u00fd F, Garnier F, Iosif R, Kuncak V, R\u00fcmmer P. A verification toolkit for numerical transition systems\u2014tool paper. In: Giannakopoulou D, M\u00e9ry D, editors. FM 2012: Formal methods\u201418th international symposium, Paris, France, August 27\u201331, 2012. Proceedings, vol. 7436. Lecture notes in computer science. Springer; 2012. pp. 247\u2013251. https:\/\/doi.org\/10.1007\/978-3-642-32759-9_21.","DOI":"10.1007\/978-3-642-32759-9_21"},{"key":"3371_CR12","doi-asserted-by":"publisher","unstructured":"Kahsai T, R\u00fcmmer P, Sanchez H, Sch\u00e4f M. Jayhorn: a framework for verifying java programs. In: Chaudhuri S, Farzan A, editors. Computer aided verification\u201428th international conference, CAV 2016, Toronto, ON, Canada, July 17\u201323, 2016, proceedings, part I, vol. 9779. Lecture notes in computer science. Springer; 2016. pp. 352\u2013358. https:\/\/doi.org\/10.1007\/978-3-319-41528-4_19.","DOI":"10.1007\/978-3-319-41528-4_19"},{"key":"3371_CR13","doi-asserted-by":"publisher","unstructured":"Kobayashi N, Sato R, Unno H. Predicate abstraction and CEGAR for higher-order model checking. In: Hall MW, Padua DA, editors. Proceedings of the 32nd ACM SIGPLAN conference on programming language design and implementation, PLDI 2011, San Jose, CA, USA, June 4\u20138. ACM; 2011. pp. 222\u2013233. https:\/\/doi.org\/10.1145\/1993498.1993525.","DOI":"10.1145\/1993498.1993525"},{"key":"3371_CR14","doi-asserted-by":"publisher","unstructured":"Matsushita Y, Tsukada T, Kobayashi N. RustHorn: CHC-based verification for rust programs. In: M\u00fcller P, editor. Programming languages and systems\u201429th European symposium on programming, ESOP 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25\u201330, 2020. Proceedings, vol. 2075. Lecture notes in computer science. Springer; 2020. pp. 484\u2013514. https:\/\/doi.org\/10.1007\/978-3-030-44914-8_18.","DOI":"10.1007\/978-3-030-44914-8_18"},{"key":"3371_CR15","doi-asserted-by":"publisher","unstructured":"De Angelis E, K, HGV. CHC-COMP 2022: competition report. In: Hamilton GW, Kahsai T, Proietti M, editors. Proceedings 9th workshop on horn clauses for verification and synthesis and 10th international workshop on verification and program transformation, HCVS\/VPT@ETAPS 2022, and 10th international workshop on verification and program transformation, Munich, Germany, 3rd April 2022. EPTCS; 2022. pp. 373:44\u201362. https:\/\/doi.org\/10.4204\/EPTCS.373.5.","DOI":"10.4204\/EPTCS.373.5"},{"key":"3371_CR16","doi-asserted-by":"publisher","unstructured":"Inverso O, La Torre S, Parlato G, Tomasco E. Verifying programs by bounded tree-width behavior graphs. In: Malvone V, Murano A, editors. Multi-agent systems\u201420th European conference, EUMAS 2023, Naples, Italy, September 14\u201315, 2023. Proceedings, vol. 14282. Lecture notes in computer science. Springer; 2023. pp. 116\u2013132. https:\/\/doi.org\/10.1007\/978-3-031-43264-4_8.","DOI":"10.1007\/978-3-031-43264-4_8"},{"key":"3371_CR17","doi-asserted-by":"crossref","unstructured":"Manna Z, Zarba CG. Combining decision procedures. In: Formal methods at the crossroads. From Panacea to Foundational Support, 10th anniversary colloquium of UNU\/IIST, The International Institute for Software Technology of The United Nations University, Lisbon, Portugal, March 18\u201320, 2002, revised papers, vol. 2757. LNCS. Springer; 2002. pp. 381\u2013422.","DOI":"10.1007\/978-3-540-40007-3_24"},{"issue":"9","key":"3371_CR18","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L Lamport","year":"1979","unstructured":"Lamport L. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans Comput. 1979;28(9):690\u20131. https:\/\/doi.org\/10.1109\/TC.1979.1675439.","journal-title":"IEEE Trans Comput"},{"key":"3371_CR19","doi-asserted-by":"publisher","unstructured":"La Torre S, Madhusudan P, Parlato G. A robust class of context-sensitive languages. In: 22nd IEEE symposium on logic in computer science (LICS 2007), 10\u201312 July 2007, Wroclaw, Poland, proceedings. IEEE Computer Society; 2007. pp. 161\u2013170. https:\/\/doi.org\/10.1109\/LICS.2007.9.","DOI":"10.1109\/LICS.2007.9"},{"issue":"8","key":"3371_CR20","doi-asserted-by":"publisher","first-page":"945","DOI":"10.1142\/S0129054117500332","volume":"28","author":"MF Atig","year":"2017","unstructured":"Atig MF, Bollig B, Habermehl P. Emptiness of ordered multi-pushdown automata is 2etime-complete. Int J Found Comput Sci. 2017;28(8):945\u201376. https:\/\/doi.org\/10.1142\/S0129054117500332.","journal-title":"Int J Found Comput Sci"},{"key":"3371_CR21","doi-asserted-by":"publisher","unstructured":"Qadeer S, Wu D. KISS: keep it simple and sequential. In: Pugh WW, Chambers C, editors. Proceedings of the ACM SIGPLAN 2004 conference on programming language design and implementation 2004, Washington, DC, USA, June 9\u201311, 2004. ACM; 2004. pp. 14\u201324. https:\/\/doi.org\/10.1145\/996841.996845.","DOI":"10.1145\/996841.996845"},{"issue":"1","key":"3371_CR22","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/S10703-009-0078-9","volume":"35","author":"A Lal","year":"2009","unstructured":"Lal A, Reps TW. Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods Syst Des. 2009;35(1):73\u201397. https:\/\/doi.org\/10.1007\/S10703-009-0078-9.","journal-title":"Formal Methods Syst Des"},{"key":"3371_CR23","doi-asserted-by":"publisher","unstructured":"La Torre S, Madhusudan P, Parlato G. Reducing context-bounded concurrent reachability to sequential reachability. In: Bouajjani A, Maler O, editors. Computer aided verification, 21st international conference, CAV 2009, Grenoble, France, June 26\u2013July 2, 2009. Proceedings, vol. 5643. Lecture notes in computer science. Springer; 2009. pp. 477\u2013492. https:\/\/doi.org\/10.1007\/978-3-642-02658-4_36.","DOI":"10.1007\/978-3-642-02658-4_36"},{"key":"3371_CR24","doi-asserted-by":"publisher","unstructured":"Emmi M, Qadeer S, Rakamaric Z. Delay-bounded scheduling. In: Ball T, Sagiv M, editors. Proceedings of the 38th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2011, Austin, TX, USA, January 26\u201328, 2011. ACM; 2011. pp. 411\u2013422. https:\/\/doi.org\/10.1145\/1926385.1926432.","DOI":"10.1145\/1926385.1926432"},{"key":"3371_CR25","doi-asserted-by":"publisher","unstructured":"La Torre S, Napoli M. Reachability of multistack pushdown systems with scope-bounded matching relations. In: Katoen J, K\u00f6nig B, editors. CONCUR 2011\u2014concurrency theory\u201422nd international conference, CONCUR 2011, Aachen, Germany, September 6\u20139, 2011. Proceedings, vol. 6901. Lecture notes in computer science. Springer; 2011. pp. 203\u2013218. https:\/\/doi.org\/10.1007\/978-3-642-23217-6_14.","DOI":"10.1007\/978-3-642-23217-6_14"},{"key":"3371_CR26","doi-asserted-by":"publisher","unstructured":"La Torre S, Parlato G. Scope-bounded multistack pushdown systems: fixed-point, sequentialization, and tree-width. In: D\u2019Souza D, Kavitha T, Radhakrishnan J, editors. IARCS annual conference on foundations of software technology and theoretical computer science, FSTTCS 2012, December 15\u201317, 2012, Hyderabad, India, vol. 18. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik; 2012. pp. 173\u2013184. https:\/\/doi.org\/10.4230\/LIPICS.FSTTCS.2012.173.","DOI":"10.4230\/LIPICS.FSTTCS.2012.173"},{"issue":"2","key":"3371_CR27","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1142\/S0129054116400074","volume":"27","author":"S La Torre","year":"2016","unstructured":"La Torre S, Napoli M, Parlato G. Scope-bounded pushdown languages. Int J Found Comput Sci. 2016;27(2):215\u201334. https:\/\/doi.org\/10.1142\/S0129054116400074.","journal-title":"Int J Found Comput Sci"},{"key":"3371_CR28","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2020.104588","volume":"275","author":"S La Torre","year":"2020","unstructured":"La Torre S, Napoli M, Parlato G. Reachability of scope-bounded multistack pushdown systems. Inf Comput. 2020;275: 104588. https:\/\/doi.org\/10.1016\/J.IC.2020.104588.","journal-title":"Inf Comput"},{"key":"3371_CR29","doi-asserted-by":"publisher","unstructured":"Bouajjani A, Emmi M, Parlato G. On sequentializing concurrent programs. In: Yahav E, editor. Static analysis\u201418th international symposium, SAS 2011, Venice, Italy, September 14\u201316, 2011. Proceedings, vol. 6887. Lecture notes in computer science. Springer; 2011. pp. 129\u2013145. https:\/\/doi.org\/10.1007\/978-3-642-23702-7_13.","DOI":"10.1007\/978-3-642-23702-7_13"},{"key":"3371_CR30","series-title":"Texts in theoretical computer science. An EATCS series","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-29953-X","volume-title":"Parameterized complexity theory","author":"J Flum","year":"2006","unstructured":"Flum J, Grohe M. Parameterized complexity theory. Texts in theoretical computer science. An EATCS series. Berlin: Springer; 2006. https:\/\/doi.org\/10.1007\/3-540-29953-X."},{"key":"3371_CR31","doi-asserted-by":"publisher","unstructured":"Musuvathi M, Qadeer S. Iterative context bounding for systematic testing of multithreaded programs. In: Ferrante J, McKinley KS, editors. Proceedings of the ACM SIGPLAN 2007 conference on programming language design and implementation, San Diego, California, USA, June 10\u201313, 2007. ACM; 2007. pp. 446\u2013455. https:\/\/doi.org\/10.1145\/1250734.1250785.","DOI":"10.1145\/1250734.1250785"},{"key":"3371_CR32","doi-asserted-by":"publisher","unstructured":"Qadeer S, Rehof J. Context-bounded model checking of concurrent software. In: Halbwachs N, Zuck LD, editors. Tools and algorithms for the construction and analysis of systems, 11th international conference, TACAS 2005, held as part of the joint European conferences on theory and practice of software, ETAPS 2005, Edinburgh, UK, April 4\u20138, 2005. Proceedings, vol. 3440. Lecture notes in computer science. Springer; 2005. pp. 93\u2013107. Springer. https:\/\/doi.org\/10.1007\/978-3-540-31980-1_7.","DOI":"10.1007\/978-3-540-31980-1_7"},{"issue":"1","key":"3371_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3478536","volume":"44","author":"O Inverso","year":"2022","unstructured":"Inverso O, Tomasco E, Fischer B, La Torre S, Parlato G. Bounded verification of multi-threaded programs via lazy sequentialization. ACM Trans Program Lang Syst. 2022;44(1):1\u20131150. https:\/\/doi.org\/10.1145\/3478536.","journal-title":"ACM Trans Program Lang Syst"},{"key":"3371_CR34","doi-asserted-by":"publisher","unstructured":"La Torre S, Napoli M, Parlato G. A unifying approach for multistack pushdown automata. In: Csuhaj-Varj\u00fa E, Dietzfelbinger M, \u00c9sik Z, editors. Mathematical foundations of computer science 2014\u201439th international symposium, MFCS 2014, Budapest, Hungary, August 25\u201329, 2014. Proceedings, part I, vol. 8634. Lecture notes in computer science. Springer; 2014. pp. 377\u2013389. https:\/\/doi.org\/10.1007\/978-3-662-44522-8_32.","DOI":"10.1007\/978-3-662-44522-8_32"},{"key":"3371_CR35","doi-asserted-by":"publisher","unstructured":"Tomasco E, Inverso O, Fischer B, La Torre S, Parlato G. Verifying concurrent programs by memory unwinding. In: Baier C, Tinelli C, editors. Tools and algorithms for the construction and analysis of systems\u201421st international conference, TACAS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11\u201318, 2015. Proceedings, vol. 9035. Lecture notes in computer science. Springer; 2015. pp. 551\u2013565. https:\/\/doi.org\/10.1007\/978-3-662-46681-0_52 .","DOI":"10.1007\/978-3-662-46681-0_52"},{"key":"3371_CR36","doi-asserted-by":"publisher","unstructured":"Enea C, Habermehl P, Inverso O, Parlato G. On the path-width of integer linear programming. In: Peron A, Piazza C, editors. Proceedings fifth international symposium on games, automata, logics and formal verification, GandALF 2014, Verona, Italy, September 10\u201312, 2014, vol. 161. EPTCS; 2014. pp. 74\u201387. https:\/\/doi.org\/10.4204\/EPTCS.161.9.","DOI":"10.4204\/EPTCS.161.9"},{"key":"3371_CR37","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/j.ic.2016.07.010","volume":"253","author":"C Enea","year":"2017","unstructured":"Enea C, Habermehl P, Inverso O, Parlato G. On the path-width of integer linear programming. Inf Comput. 2017;253:257\u201371. https:\/\/doi.org\/10.1016\/j.ic.2016.07.010.","journal-title":"Inf Comput"},{"issue":"1","key":"3371_CR38","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1016\/0890-5401(90)90043-H","volume":"85","author":"B Courcelle","year":"1990","unstructured":"Courcelle B. The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf Comput. 1990;85(1):12\u201375. https:\/\/doi.org\/10.1016\/0890-5401(90)90043-H.","journal-title":"Inf Comput"},{"issue":"2","key":"3371_CR39","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0168-0072(91)90054-P","volume":"53","author":"D Seese","year":"1991","unstructured":"Seese D. The structure of models of decidable monadic theories of graphs. Ann Pure Appl Log. 1991;53(2):169\u201395. https:\/\/doi.org\/10.1016\/0168-0072(91)90054-P.","journal-title":"Ann Pure Appl Log"},{"key":"3371_CR40","doi-asserted-by":"publisher","unstructured":"Gurfinkel A. Program verification with constrained Horn clauses (invited paper). In: Shoham S, Vizel Y, editors. Computer aided verification\u201434th international conference, CAV 2022, Haifa, Israel, August 7\u201310, 2022. Proceedings, part I, vol. 1337. Lecture notes in computer science. Springer; 2022. pp. 19\u201329. https:\/\/doi.org\/10.1007\/978-3-031-13185-1_2.","DOI":"10.1007\/978-3-031-13185-1_2"},{"key":"3371_CR41","doi-asserted-by":"publisher","unstructured":"La Torre S, Madhusudan P, Parlato G. Analyzing recursive programs using a fixed-point calculus. In: Hind M, Diwan A, editors. Proceedings of the 2009 ACM SIGPLAN conference on programming language design and implementation, PLDI 2009, Dublin, Ireland, June 15\u201321, 2009. ACM; 2009. pp. 211\u2013222. https:\/\/doi.org\/10.1145\/1542476.1542500.","DOI":"10.1145\/1542476.1542500"},{"key":"3371_CR42","doi-asserted-by":"publisher","unstructured":"Moura LM, Bj\u00f8rner N. Z3: an efficient SMT solver. In: Ramakrishnan CR, Rehof J, editors. Tools and algorithms for the construction and analysis of systems, 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29\u2013April 6, 2008. Proceedings, vol. 4963. Lecture notes in computer science. Springer; 2008. pp. 337\u2013340. https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"3371_CR43","doi-asserted-by":"publisher","unstructured":"Blicha M, Britikov K, Sharygina N. The Golem Horn solver. In: Enea C, Lal A, editors. Computer aided verification\u201435th international conference, CAV 2023, Paris, France, July 17\u201322, 2023. Proceedings, part II, vol. 13965. Lecture notes in computer science. Springer; 2023. pp. 209\u2013223. https:\/\/doi.org\/10.1007\/978-3-031-37703-7_10.","DOI":"10.1007\/978-3-031-37703-7_10"},{"key":"3371_CR44","doi-asserted-by":"publisher","unstructured":"Hojjat H, R\u00fcmmer P. The ELDARICA Horn solver. In: Bj\u00f8rner NS, Gurfinkel A, editors. 2018 Formal methods in computer aided design, FMCAD 2018, Austin, TX, USA, October 30\u2013November 2, 2018. IEEE; 2018. pp. 1\u20137. https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013.","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"3371_CR45","doi-asserted-by":"publisher","unstructured":"Henn T, V\u00f6lker M, Kowalewski S, Trinh M, Petrovic O, Brecher C. Verification of behavior trees using linear constrained horn clauses. In: Groote JF, Huisman M, editors. Formal methods for industrial critical systems\u201427th international conference, FMICS 2022, Warsaw, Poland, 2022, 14\u201315. Proceedings, vol. 13487. Lecture notes in computer science. Springer; 2022. pp. 211\u2013225. https:\/\/doi.org\/10.1007\/978-3-031-15008-1_14.","DOI":"10.1007\/978-3-031-15008-1_14"},{"key":"3371_CR46","doi-asserted-by":"publisher","unstructured":"Faella M, Parlato G. Reachability games modulo theories with a bounded safety player. In: Williams B, Chen Y, Neville J, editors. Thirty-seventh AAAI conference on artificial intelligence, AAAI 2023, thirty-fifth conference on innovative applications of artificial intelligence, IAAI 2023, thirteenth symposium on educational advances in artificial intelligence, EAAI 2023, Washington, DC, USA, February 7\u201314, 2023. AAAI Press; 2023. pp. 6330\u20136337. https:\/\/doi.org\/10.1609\/AAAI.V37I5.25779.","DOI":"10.1609\/AAAI.V37I5.25779"},{"key":"3371_CR47","doi-asserted-by":"publisher","unstructured":"Tomasco E, Nguyen TL, Inverso O, Fischer B, La Torre S, Parlato G. Lazy sequentialization for TSO and PSO via shared memory abstractions. In: Piskac R, Talupur M, editors. 2016 Formal methods in computer-aided design, FMCAD 2016, Mountain View, CA, USA, October 3\u20136, 2016. IEEE; 2016. pp. 193\u2013200. https:\/\/doi.org\/10.1109\/FMCAD.2016.7886679.","DOI":"10.1109\/FMCAD.2016.7886679"},{"key":"3371_CR48","doi-asserted-by":"publisher","unstructured":"Tomasco E, Nguyen TL, Fischer B, La Torre S, Parlato G. Using shared memory abstractions to design eager sequentializations for weak memory models. In: Cimatti A, Sirjani M, editors. Software engineering and formal methods\u201415th international conference, SEFM 2017, Trento, Italy, September 4\u20138, 2017. Proceedings, vol. 10469. Lecture notes in computer science. Springer; 2017. pp. 185\u2013202. Springer https:\/\/doi.org\/10.1007\/978-3-319-66197-1_12.","DOI":"10.1007\/978-3-319-66197-1_12"},{"key":"3371_CR49","doi-asserted-by":"publisher","unstructured":"Komuravelli A, Bj\u00f8rner NS, Gurfinkel A, McMillan KL. Compositional verification of procedural programs using horn clauses over integers and arrays. In: Kaivola R, Wahl T, editors. Formal methods in computer-aided design, FMCAD 2015, Austin, Texas, USA, September 27\u201330. IEEE; 2015. pp. 89\u201396. https:\/\/doi.org\/10.1109\/FMCAD.2015.7542257.","DOI":"10.1109\/FMCAD.2015.7542257"},{"issue":"1","key":"3371_CR50","doi-asserted-by":"publisher","first-page":"73","DOI":"10.3233\/FI-2017-1461","volume":"150","author":"E De Angelis","year":"2017","unstructured":"De Angelis E, Fioravanti F, Pettorossi A, Proietti M. Program verification using constraint handling rules and array constraint generalizations. Fundam Inform. 2017;150(1):73\u2013117. https:\/\/doi.org\/10.3233\/FI-2017-1461.","journal-title":"Fundam Inform"},{"key":"3371_CR51","doi-asserted-by":"crossref","unstructured":"Faella M, Parlato G. A unified automata-theoretic approach to LTLf modulo theories. In: ECAI 2024\u201427th European conference on artificial intelligence, October 19\u201324, 2024. Santiago de Compostela, Spain. Frontiers in artificial intelligence and applications. IOS Press; 2024.","DOI":"10.3233\/FAIA240622"}],"container-title":["SN Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s42979-024-03371-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s42979-024-03371-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s42979-024-03371-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T17:06:49Z","timestamp":1731949609000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s42979-024-03371-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,18]]},"references-count":51,"journal-issue":{"issue":"8","published-online":{"date-parts":[[2024,12]]}},"alternative-id":["3371"],"URL":"https:\/\/doi.org\/10.1007\/s42979-024-03371-6","relation":{},"ISSN":["2661-8907"],"issn-type":[{"type":"electronic","value":"2661-8907"}],"subject":[],"published":{"date-parts":[[2024,11,18]]},"assertion":[{"value":"21 March 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 September 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 November 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"On behalf of all authors, the corresponding author states that there is no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"This article does not contain any studies with human participants or animals performed by any of the authors.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Research involving human and \/or animals"}},{"value":"Not applicable.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Informed consent"}}],"article-number":"1062"}}