{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:07:47Z","timestamp":1776305267777,"version":"3.50.1"},"reference-count":69,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T00:00:00Z","timestamp":1742947200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T00:00:00Z","timestamp":1742947200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001824","name":"Grantov\u00e1 Agentura \u010cesk\u00e9 Republiky","doi-asserted-by":"publisher","award":["23-06506 S"],"award-info":[{"award-number":["23-06506 S"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001711","name":"Schweizerischer Nationalfonds zur F\u00f6rderung der Wissenschaftlichen Forschung","doi-asserted-by":"publisher","award":["200021_185031"],"award-info":[{"award-number":["200021_185031"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001711","name":"Schweizerischer Nationalfonds zur F\u00f6rderung der Wissenschaftlichen Forschung","doi-asserted-by":"publisher","award":["200021_185031"],"award-info":[{"award-number":["200021_185031"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001711","name":"Schweizerischer Nationalfonds zur F\u00f6rderung der Wissenschaftlichen Forschung","doi-asserted-by":"publisher","award":["200021_185031"],"award-info":[{"award-number":["200021_185031"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100030993","name":"Universit\u00e0 della Svizzera italiana","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100030993","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    The logical framework of Constrained Horn Clauses (CHC) models verification tasks from a variety of domains, ranging from verification of safety properties in transition systems to modular verification of programs with procedures. In this work we present G\n                    <jats:sc>olem<\/jats:sc>\n                    , a flexible and efficient solver for satisfiability of CHCs over linear real and integer arithmetic. G\n                    <jats:sc>olem<\/jats:sc>\n                    provides flexibility with modular architecture and multiple back-end model-checking algorithms, as well as efficiency with tight integration with the underlying SMT solver. This paper describes the architecture of G\n                    <jats:sc>olem<\/jats:sc>\n                    and its back-end engines, which include our recently introduced model-checking algorithm TPA for deep exploration. The description is complemented by extensive evaluation, demonstrating the competitive nature of the solver.\n                  <\/jats:p>","DOI":"10.1007\/s10703-025-00470-9","type":"journal-article","created":{"date-parts":[[2025,3,29]],"date-time":"2025-03-29T12:48:09Z","timestamp":1743252489000},"page":"143-160","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Golem: a flexible and efficient solver for constrained Horn clauses"],"prefix":"10.1007","volume":"67","author":[{"given":"Martin","family":"Blicha","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Konstantin","family":"Britikov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,3,26]]},"reference":[{"key":"470_CR1","doi-asserted-by":"publisher","unstructured":"Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: Proceedings of the 33rd ACM SIGPLAN conference on programming language design and implementation. PLDI \u201912, pp. 405\u2013416. Association for computing machinery, New York, NY, USA. https:\/\/doi.org\/10.1145\/2254064.2254112","DOI":"10.1145\/2254064.2254112"},{"key":"470_CR2","doi-asserted-by":"publisher","unstructured":"Gurfinkel A, Bj\u00f8rner N (2019) The science, art, and magic of constrained Horn clauses. In: 2019 21st International symposium on symbolic and numeric algorithms for scientific computing (SYNASC), pp. 6\u201310. https:\/\/doi.org\/10.1109\/SYNASC49474.2019.00010","DOI":"10.1109\/SYNASC49474.2019.00010"},{"key":"470_CR3","doi-asserted-by":"publisher","first-page":"39","DOI":"10.4204\/EPTCS.169.6","volume":"169","author":"H Hojjat","year":"2014","unstructured":"Hojjat H, R\u00fcmmer P, Subotic P, Yi W (2014) Horn clauses for communicating timed systems. Electron Proc Theor Comput Sci 169:39\u201352. https:\/\/doi.org\/10.4204\/EPTCS.169.6","journal-title":"Electron Proc Theor Comput Sci"},{"key":"470_CR4","doi-asserted-by":"publisher","unstructured":"Gurfinkel A (2022) Program verification with constrained Horn clauses (invited paper). In: Shoham S, Vizel Y (eds.) Computer aided verification, pp. 19\u201329. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-031-13185-1_2","DOI":"10.1007\/978-3-031-13185-1_2"},{"key":"470_CR5","doi-asserted-by":"publisher","unstructured":"Gurfinkel A, Kahsai T, Komuravelli A, Navas JA (2015) The SeaHorn verification framework. In: Kroening D, P\u0103s\u0103reanu CS (eds.) Computer aided verification, pp. 343\u2013361. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"470_CR6","doi-asserted-by":"publisher","unstructured":"Ernst G (2023) Korn\u2014software verification with Horn clauses (competition contribution). In: Sankaranarayanan S, Sharygina N (eds.) Tools and algorithms for the construction and analysis of systems, pp. 559\u2013564. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-031-30820-8_36","DOI":"10.1007\/978-3-031-30820-8_36"},{"key":"470_CR7","doi-asserted-by":"publisher","unstructured":"Esen Z, R\u00fcmmer P (2022) TriCera: verifying C programs using the theory of heaps. In: Griggio A, Rungta N (eds.) Proceedings of the 22nd conference on formal methods in computer-aided design\u2014FMCAD 2022, pp. 360\u2013391. TU Wien Academic Press, Vienna. https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_45","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_45"},{"key":"470_CR8","doi-asserted-by":"publisher","unstructured":"Kahsai T, R\u00fcmmer P, Sanchez H, Sch\u00e4f M (2016) JayHorn: a framework for verifying Java programs. In: Chaudhuri S, Farzan A (eds.) Computer aided verification, pp. 352\u2013358. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-319-41528-4_19","DOI":"10.1007\/978-3-319-41528-4_19"},{"key":"470_CR9","doi-asserted-by":"publisher","DOI":"10.1145\/3462205","author":"Y Matsushita","year":"2021","unstructured":"Matsushita Y, Tsukada T, Kobayashi N (2021) RustHorn: CHC-based verification for Rust programs. ACM Trans Program Lang Syst. https:\/\/doi.org\/10.1145\/3462205","journal-title":"ACM Trans Program Lang Syst"},{"key":"470_CR10","doi-asserted-by":"publisher","unstructured":"Calzavara S, Grishchenko I, Maffei M (2016) HornDroid: practical and sound static analysis of android applications by SMT solving. In: 2016 IEEE European symposium on security and privacy, pp. 47\u201362. https:\/\/doi.org\/10.1109\/EUROSP.2016.16","DOI":"10.1109\/EUROSP.2016.16"},{"key":"470_CR11","doi-asserted-by":"publisher","unstructured":"Alt L, Blicha M, Hyv\u00e4rinen AEJ, Sharygina N (2022) SolCMC: solidity compiler\u2019s model checker. In: Shoham S, Vizel Y (eds.) Computer aided verification, pp. 325\u2013338. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-031-13185-1_16","DOI":"10.1007\/978-3-031-13185-1_16"},{"key":"470_CR12","doi-asserted-by":"publisher","unstructured":"Wesley S, Christakis M, Navas JA, Trefler R, W\u00fcstholz V, Gurfinkel A (2022) Verifying Solidity smart contracts via communication abstraction in SmartACE. In: Finkbeiner B, Wies T (eds.) Verification, model checking, and abstract interpretation, pp. 425\u2013449. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-030-94583-1_21","DOI":"10.1007\/978-3-030-94583-1_21"},{"key":"470_CR13","doi-asserted-by":"publisher","unstructured":"Zlatkin I, Fedyukovich G (2022) Maximizing branch coverage with constrained Horn clauses. In: Fisman D, Rosu G (eds.) Tools and algorithms for the construction and analysis of systems, pp. 254\u2013272. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-030-99527-0_14","DOI":"10.1007\/978-3-030-99527-0_14"},{"key":"470_CR14","doi-asserted-by":"publisher","unstructured":"Graf S, Saidi H (1997) Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) Computer aided verification, pp. 72\u201383. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/3-540-63166-6_10","DOI":"10.1007\/3-540-63166-6_10"},{"key":"470_CR15","doi-asserted-by":"publisher","unstructured":"Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Emerson EA, Sistla AP (eds.) Computer aided verification, pp. 154\u2013169. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/10722167_15","DOI":"10.1007\/10722167_15"},{"key":"470_CR16","doi-asserted-by":"publisher","unstructured":"Bradley AR (2011) SAT-based model checking without unrolling. In: Jhala R, Schmidt D (eds.) Verification, model checking, and abstract interpretation, pp. 70\u201387. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"470_CR17","unstructured":"E\u00e9n N, Mishchenko A, Brayton R (2011) Efficient implementation of property directed reachability. In: Proceedings of the international conference on formal methods in computer-aided design. FMCAD \u201911, pp. 125\u2013134. FMCAD Inc, Austin, TX"},{"key":"470_CR18","doi-asserted-by":"publisher","unstructured":"Hojjat H, R\u00fcmmer P (2018) The Eldarica Horn solver. In: FMCAD, pp. 158\u2013164. IEEE, New York City. https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013","DOI":"10.23919\/FMCAD.2018.8603013"},{"issue":"3","key":"470_CR19","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig W (1957) Three uses of the Herbrand\u2013Gentzen theorem in relating model theory and proof theory. J Symbol Logic 22(3):269\u2013285","journal-title":"J Symbol Logic"},{"key":"470_CR20","doi-asserted-by":"publisher","unstructured":"Hojjat H, Iosif R, Kone\u010dn\u00fd F, Kuncak V, R\u00fcmmer P (2012) Accelerating interpolants. In: Chakraborty S, Mukund M (eds.) Automated technology for verification and analysis, pp. 187\u2013202. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-642-33386-6_16","DOI":"10.1007\/978-3-642-33386-6_16"},{"key":"470_CR21","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer P, Suboti\u0107 P (2013) Exploring interpolants. In: 2013 Formal methods in computer-aided design, pp. 69\u201376","DOI":"10.1109\/FMCAD.2013.6679393"},{"issue":"4","key":"470_CR22","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/S00236-015-0236-Z","volume":"53","author":"J Leroux","year":"2016","unstructured":"Leroux J, R\u00fcmmer P, Suboti\u0107 P (2016) Guiding Craig interpolation with domain-specific abstractions. Acta Informatica 53(4):387\u2013424. https:\/\/doi.org\/10.1007\/S00236-015-0236-Z","journal-title":"Acta Informatica"},{"issue":"3","key":"470_CR23","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/S10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli A, Gurfinkel A, Chaki S (2016) SMT-based model checking for recursive programs. Formal Methods Syst Design 48(3):175\u2013205. https:\/\/doi.org\/10.1007\/S10703-016-0249-4","journal-title":"Formal Methods Syst Design"},{"key":"470_CR24","doi-asserted-by":"publisher","unstructured":"Moura L, Bj\u00f8rner N (2008) Z3: An efficient SMT solver. In: Ramakrishnan CR, Rehof J (eds.) Tools and algorithms for the construction and analysis of systems, pp. 337\u2013340. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"470_CR25","doi-asserted-by":"publisher","unstructured":"Hoder K, Bj\u00f8rner N (2012) Generalized property directed reachability. In: Cimatti A, Sebastiani R (eds.) Theory and applications of satisfiability testing\u2014SAT 2012, pp. 157\u2013171. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-642-31612-8_13","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"470_CR26","doi-asserted-by":"publisher","unstructured":"Hari\u00a0Govind VK, Chen Y, Shoham S, Gurfinkel A (2020) Global guidance for local generalization in model checking. In: Lahiri SK, Wang C (eds.) Computer aided verification, pp. 101\u2013125. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-030-53291-8_7","DOI":"10.1007\/978-3-030-53291-8_7"},{"key":"470_CR27","doi-asserted-by":"publisher","unstructured":"Dietsch D, Heizmann M, Hoenicke J, Nutz A, Podelski A (2019) Ultimate TreeAutomizer (CHC-COMP tool description). In: Angelis ED, Fedyukovich G, Tzevelekos N, Ulbrich M (eds.) Proceedings of the sixth workshop on horn clauses for verification and synthesis and third workshop on program equivalence and relational reasoning, HCVS\/PERR@ETAPS 2019, Prague, Czech Republic, 6-7th April 2019. EPTCS, vol. 296, pp. 42\u201347. https:\/\/doi.org\/10.4204\/EPTCS.296.7","DOI":"10.4204\/EPTCS.296.7"},{"key":"470_CR28","doi-asserted-by":"publisher","unstructured":"Kafle B, Gallagher JP (2015) Tree automata-based refinement with application to Horn clause verification. In: D\u2019Souza D, Lal A, Larsen KG (eds.) Verification, model checking, and abstract interpretation, pp. 209\u2013226. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-662-46081-8_12","DOI":"10.1007\/978-3-662-46081-8_12"},{"issue":"8","key":"470_CR29","doi-asserted-by":"publisher","first-page":"1236","DOI":"10.1093\/COMJNL\/BXW017","volume":"59","author":"W Wang","year":"2016","unstructured":"Wang W, Jiao L (2016) Trace abstraction refinement for solving horn clauses. Comput J 59(8):1236\u20131251. https:\/\/doi.org\/10.1093\/COMJNL\/BXW017","journal-title":"Comput J"},{"key":"470_CR30","doi-asserted-by":"publisher","unstructured":"Champion A, Kobayashi N, Sato R (2018) HoIce: an ICE-based non-linear Horn clause solver. In: Ryu S (ed.) Programming languages and systems. lecture notes in computer science, vol. 11275, pp. 146\u2013156. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-030-02768-1_8","DOI":"10.1007\/978-3-030-02768-1_8"},{"key":"470_CR31","doi-asserted-by":"publisher","unstructured":"Champion A, Chiba T, Kobayashi N, Sato R (2018) ICE-based refinement type discovery for higher-order functional programs. In: Beyer D, Huisman M (eds.) Tools and algorithms for the construction and analysis of systems, pp. 365\u2013384. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-030-02768-1_8","DOI":"10.1007\/978-3-030-02768-1_8"},{"key":"470_CR32","doi-asserted-by":"publisher","unstructured":"Fedyukovich G, Kaufman SJ, Bod\u00edk R (2017) Sampling invariants from frequency distributions. In: 2017 Formal methods in computer aided design (FMCAD), pp. 100\u2013107. https:\/\/doi.org\/10.23919\/FMCAD.2017.8102247","DOI":"10.23919\/FMCAD.2017.8102247"},{"key":"470_CR33","doi-asserted-by":"publisher","unstructured":"Fedyukovich G, Prabhu S, Madhukar K, Gupta A (2018) Solving constrained Horn clauses using syntax and data. In: 2018 Formal methods in computer aided design (FMCAD), pp. 1\u20139. https:\/\/doi.org\/10.23919\/FMCAD.2018.8603011","DOI":"10.23919\/FMCAD.2018.8603011"},{"key":"470_CR34","doi-asserted-by":"crossref","unstructured":"Alur R, Bodik R, Juniwal G, Martin MMK, Raghothaman M, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2013) Syntax-guided synthesis. In: 2013 Formal methods in computer-aided design, pp. 1\u20138","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"470_CR35","doi-asserted-by":"publisher","unstructured":"R\u00fcmmer P (2020) Competition report: CHC-COMP-20. Electronic proceedings in theoretical computer science 320, 197\u2013219 https:\/\/doi.org\/10.4204\/EPTCS.320.15","DOI":"10.4204\/EPTCS.320.15"},{"key":"470_CR36","doi-asserted-by":"publisher","unstructured":"Fedyukovich G, R\u00fcmmer P (2021) Competition report: CHC-COMP-21. In: Hojjat H, Kafle B (eds.) Proceedings 8th workshop on horn clauses for verification and synthesis, HCVS@ETAPS 2021, Virtual, 28th March 2021. EPTCS, vol. 344, pp. 91\u2013108. https:\/\/doi.org\/10.4204\/EPTCS.344.7","DOI":"10.4204\/EPTCS.344.7"},{"key":"470_CR37","doi-asserted-by":"publisher","first-page":"44","DOI":"10.4204\/EPTCS.373.5","volume":"373","author":"E De Angelis","year":"2022","unstructured":"De Angelis E, Vediramana Krishnan HG (2022) CHC-COMP 2022: competition report. Electron Proc Theor Comput Sci 373:44\u201362. https:\/\/doi.org\/10.4204\/EPTCS.373.5","journal-title":"Electron Proc Theor Comput Sci"},{"key":"470_CR38","unstructured":"Beyer D, Wendler P (2012) Algorithms for software model checking: predicate abstraction vs. Impact. In: 2012 Formal methods in computer-aided design (FMCAD), pp. 106\u2013113"},{"key":"470_CR39","doi-asserted-by":"publisher","unstructured":"Beyer D, Dangl M (2020) Software verification with PDR: an implementation of the state of the art. In: Biere A, Parker D (eds.) Tools and algorithms for the construction and analysis of systems, pp. 3\u201321. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-030-45190-5_1","DOI":"10.1007\/978-3-030-45190-5_1"},{"key":"470_CR40","doi-asserted-by":"publisher","unstructured":"Beyer D, Dangl M, Wendler P (2015) Boosting k-induction with continuously-refined invariants. In: Kroening D, P\u0103s\u0103reanu CS (eds.) Computer aided verification, pp. 622\u2013640. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-319-21690-4_42","DOI":"10.1007\/978-3-319-21690-4_42"},{"issue":"3","key":"470_CR41","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/S10817-017-9432-6","volume":"60","author":"D Beyer","year":"2018","unstructured":"Beyer D, Dangl M, Wendler P (2018) A unifying view on SMT-based software verification. J Autom Reason 60(3):299\u2013335. https:\/\/doi.org\/10.1007\/S10817-017-9432-6","journal-title":"J Autom Reason"},{"key":"470_CR42","doi-asserted-by":"publisher","unstructured":"Beyer D, Keremoglu ME (2011) CPAchecker: a tool for configurable software verification. In: Gopalakrishnan G, Qadeer S (eds.) Computer aided verification, pp. 184\u2013190. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"470_CR43","doi-asserted-by":"publisher","unstructured":"Beyer D, Lee N-Z, Wendler P (August 2022) Interpolation and SAT-based model checking revisited: adoption to software verification. Technical Report 2208.05046, arXiv\/CoRR. https:\/\/doi.org\/10.48550\/ARXIV.2208.05046","DOI":"10.48550\/ARXIV.2208.05046"},{"key":"470_CR44","doi-asserted-by":"publisher","unstructured":"Mann M, Irfan A, Lonsing F, Yang Y, Zhang H, Brown K, Gupta A, Barrett C (2021) Pono: a flexible and extensible SMT-based model checker. In: Silva A, Leino KRM (eds.) Computer aided verification, pp. 461\u2013474. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-030-81688-9_22","DOI":"10.1007\/978-3-030-81688-9_22"},{"key":"470_CR45","doi-asserted-by":"publisher","unstructured":"Blicha M, Fedyukovich G, Hyv\u00e4rinen AEJ, Sharygina N (2022) Transition power abstractions for deep counterexample detection. In: Fisman D, Rosu G (eds.) Tools and algorithms for the construction and analysis of systems, pp. 524\u2013542. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-030-99524-9_29","DOI":"10.1007\/978-3-030-99524-9_29"},{"key":"470_CR46","doi-asserted-by":"publisher","unstructured":"Blicha M, Fedyukovich G, Hyv\u00e4rinen AEJ, Sharygina N (2022) Split transition power abstractions for unbounded safety. In: Griggio A, Rungta N (eds.) Proceedings of the 22nd conference on formal methods in computer-aided design\u2014FMCAD 2022, pp. 349\u2013358. TU Wien Academic Press, Vienna. https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_42","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_42"},{"key":"470_CR47","doi-asserted-by":"publisher","unstructured":"Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDs. In: Cleaveland WR (ed.) Tools and algorithms for the construction and analysis of systems, pp. 193\u2013207. Springer, Berlin, Heidelberg.https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"470_CR48","doi-asserted-by":"publisher","unstructured":"Sheeran M, Singh S, St\u00e5lmarck G (2000) Checking safety properties using induction and a SAT-solver. In: Hunt WA, Johnson SD (eds.) Formal methods in computer-aided design, pp. 127\u2013144. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/3-540-40922-X_8","DOI":"10.1007\/3-540-40922-X_8"},{"key":"470_CR49","doi-asserted-by":"publisher","unstructured":"McMillan KL (2003) Interpolation and SAT-based model checking. In: Computer aided verification, pp. 1\u201313. Springer, Berlin Heidelberg. https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"470_CR50","doi-asserted-by":"publisher","unstructured":"McMillan KL (2006) Lazy abstraction with interpolants. In: Ball T, Jones RB (eds.) Computer aided verification, pp. 123\u2013136. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/11817963_14","DOI":"10.1007\/11817963_14"},{"key":"470_CR51","doi-asserted-by":"publisher","unstructured":"Bruttomesso R, Pek E, Sharygina N, Tsitovich A (2010) The OpenSMT solver. In: Esparza J, Majumdar R (eds.) Tools and algorithms for the construction and analysis of systems, pp. 150\u2013153. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-642-12002-2_12","DOI":"10.1007\/978-3-642-12002-2_12"},{"key":"470_CR52","doi-asserted-by":"publisher","unstructured":"Hyv\u00e4rinen AEJ, Marescotti M, Alt L, Sharygina N (2016) OpenSMT2: an SMT solver for multi-core and cloud computing. In: Creignou N, Le\u00a0Berre D (eds.) Theory and applications of satisfiability testing\u2014SAT 2016, pp. 547\u2013553. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-319-40970-2_35","DOI":"10.1007\/978-3-319-40970-2_35"},{"key":"470_CR53","doi-asserted-by":"publisher","unstructured":"Blicha M, Britikov K, Sharygina N (2023) The Golem Horn solver. In: Enea C, Lal A (eds.) Computer aided verification, pp. 209\u2013223. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-031-37703-7_10","DOI":"10.1007\/978-3-031-37703-7_10"},{"issue":"1","key":"470_CR54","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/S10703-014-0219-7","volume":"47","author":"P R\u00fcmmer","year":"2015","unstructured":"R\u00fcmmer P, Hojjat H, Kuncak V (2015) On recursion-free Horn clauses and Craig interpolation. Form Methods Syst Design 47(1):1\u201325. https:\/\/doi.org\/10.1007\/S10703-014-0219-7","journal-title":"Form Methods Syst Design"},{"key":"470_CR55","unstructured":"Alt L (2016) Controlled and effective interpolation. PhD thesis, Universit\u00e0 della Svizzera italiana. Available at https:\/\/susi.usi.ch\/usi\/documents\/318933"},{"key":"470_CR56","unstructured":"Barrett C, Fontaine P, Tinelli C (2017) The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa. Available at www.SMT-LIB.org"},{"issue":"1","key":"470_CR57","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/565816.503279","volume":"37","author":"TA Henzinger","year":"2002","unstructured":"Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. SIGPLAN Not. 37(1):58\u201370. https:\/\/doi.org\/10.1145\/565816.503279","journal-title":"SIGPLAN Not."},{"key":"470_CR58","doi-asserted-by":"publisher","unstructured":"Komuravelli A, Gurfinkel A, Chaki S (2014) SMT-based model checking for recursive programs. In: Biere A, Bloem R (eds.) Computer aided verification, pp. 17\u201334. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-319-08867-9_2","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"470_CR59","doi-asserted-by":"publisher","unstructured":"Komuravelli A, Bj\u00f8rner N, Gurfinkel A, McMillan KL (2015) Compositional verification of procedural programs using Horn clauses over integers and arrays. In: 2015 Formal methods in computer-aided design (FMCAD), pp. 89\u201396. https:\/\/doi.org\/10.1109\/FMCAD.2015.7542257","DOI":"10.1109\/FMCAD.2015.7542257"},{"key":"470_CR60","doi-asserted-by":"publisher","unstructured":"Vediramana\u00a0Krishnan HG, Fedyukovich G, Gurfinkel A (2020) Word level property directed reachability. In: 2020 IEEE\/ACM international conference on computer aided design (ICCAD), pp. 1\u20139. https:\/\/doi.org\/10.1145\/3400302.3415708","DOI":"10.1145\/3400302.3415708"},{"key":"470_CR61","doi-asserted-by":"publisher","unstructured":"Vediramana\u00a0Krishnan HG, Shoham S, Gurfinkel A (2022) Solving constrained Horn clauses modulo algebraic data types and recursive functions. Proc. ACM Program. Lang. 6(POPL) https:\/\/doi.org\/10.1145\/3498722","DOI":"10.1145\/3498722"},{"key":"470_CR62","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner N, Janota M (2015) Playing with quantified satisfaction. In: Fehnker A, McIver A, Sutcliffe G, Voronkov A (eds.) LPAR-20. 20th international conferences on logic for programming, artificial intelligence and reasoning\u2014short presentations. EPiC Series in Computing, vol. 35, pp. 15\u201327. EasyChair, Fiji. https:\/\/doi.org\/10.29007\/VV21","DOI":"10.29007\/VV21"},{"key":"470_CR63","doi-asserted-by":"publisher","unstructured":"Rollini SF, Alt L, Fedyukovich G, Hyv\u00e4rinen AEJ, Sharygina N (2013) PeRIPLO: a framework for producing effective interpolants in SAT-based software verification. In: McMillan K, Middeldorp A, Voronkov A (eds.) Logic for programming, artificial intelligence, and reasoning, pp. 683\u2013693. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-642-45221-5_45","DOI":"10.1007\/978-3-642-45221-5_45"},{"key":"470_CR64","doi-asserted-by":"publisher","unstructured":"Alt L, Hyv\u00e4rinen AEJ, Sharygina N (2017) LRA interpolants from no man\u2019s land. In: Strichman O, Tzoref-Brill R (eds.) Hardware and software: verification and testing, pp. 195\u2013210. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-319-70389-3_13","DOI":"10.1007\/978-3-319-70389-3_13"},{"issue":"1","key":"470_CR65","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/S10009-021-00641-Z","volume":"24","author":"M Blicha","year":"2022","unstructured":"Blicha M, Hyv\u00e4rinen AEJ, Kofro\u0148 J, Sharygina N (2022) Using linear algebra in decomposition of Farkas interpolants. Int J Softw Tools Technol Transfer 24(1):111\u2013125. https:\/\/doi.org\/10.1007\/S10009-021-00641-Z","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"470_CR66","doi-asserted-by":"publisher","unstructured":"Jhala R, McMillan KL (2006) A practical and complete approach to predicate refinement. In: Hermanns H, Palsberg J (eds.) Tools and algorithms for the construction and analysis of systems, pp. 459\u2013473. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/11691372_33","DOI":"10.1007\/11691372_33"},{"key":"470_CR67","doi-asserted-by":"publisher","unstructured":"Vizel Y, Grumberg O (2009) Interpolation-sequence based model checking. In: Formal methods in computer-aided design, pp. 1\u20138. IEEE, New York City, United States . https:\/\/doi.org\/10.1109\/FMCAD.2009.5351148","DOI":"10.1109\/FMCAD.2009.5351148"},{"key":"470_CR68","unstructured":"Cimatti A, Griggio A, Tonetta S (2021) The VMT-LIB language and tools. arxiv:2109.12821"},{"key":"470_CR69","doi-asserted-by":"publisher","unstructured":"Jovanovi\u0107 D, Dutertre B (2016) Property-directed k-induction. In: 2016 formal methods in computer-aided design (FMCAD), pp. 85\u201392. https:\/\/doi.org\/10.1109\/FMCAD.2016.7886665","DOI":"10.1109\/FMCAD.2016.7886665"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00470-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-025-00470-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00470-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T05:03:14Z","timestamp":1762491794000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-025-00470-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,26]]},"references-count":69,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,11]]}},"alternative-id":["470"],"URL":"https:\/\/doi.org\/10.1007\/s10703-025-00470-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,3,26]]},"assertion":[{"value":"31 March 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 February 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 March 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}