{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:46:01Z","timestamp":1775868361531,"version":"3.50.1"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031747755","type":"print"},{"value":"9783031747762","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-74776-2_10","type":"book-chapter","created":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T05:35:50Z","timestamp":1737351350000},"page":"242-267","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Verification of\u00a0Programs with\u00a0ADTs Using Shallow Horn Clauses"],"prefix":"10.1007","author":[{"given":"Th\u00e9o","family":"Losekoot","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2145-3370","authenticated-orcid":false,"given":"Thomas","family":"Genet","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4064-7170","authenticated-orcid":false,"given":"Thomas","family":"Jensen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,1,21]]},"reference":[{"key":"10_CR1","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org"},{"issue":"1\u20132","key":"10_CR2","doi-asserted-by":"publisher","first-page":"21","DOI":"10.3233\/SAT190028","volume":"3","author":"C Barrett","year":"2007","unstructured":"Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. J. Satisfiability Boolean Model. Comput. 3(1\u20132), 21\u201346 (2007)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Bautista, S., Jensen, T., Montagu, B.: Lifting numeric relational domains to algebraic data types. In: SAS 2022. LNCS, vol. 13790, pp. 104\u2013134. Springer (2022)","DOI":"10.1007\/978-3-031-22308-2_6"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Fields of Logic and Computation II, pp. 24\u201351. Springer (2015)","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"10_CR5","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/j.jcss.2017.01.006","volume":"104","author":"Y Boichut","year":"2019","unstructured":"Boichut, Y., Chabin, J., R\u00e9ty, P.: Towards more precise rewriting approximations. J. Comput. Syst. Sci. 104, 131\u2013148 (2019)","journal-title":"J. Comput. Syst. Sci."},{"key":"10_CR6","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: Tip and isaplanner benchmarks (2015). https:\/\/tip-org.github.io\/"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-45085-6_22","volume-title":"Automated Deduction \u2013 CADE-19","author":"L Dixon","year":"2003","unstructured":"Dixon, L., Fleuriot, J.: IsaPlanner: a prototype proof planner in Isabelle. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 279\u2013283. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45085-6_22"},{"issue":"4","key":"10_CR8","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/321978.321991","volume":"23","author":"MH van Emden","year":"1976","unstructured":"van Emden, M.H., Kowalski, R.A.: The semantics of predicate logic as a programming language. J. ACM 23(4), 733\u2013742 (1976)","journal-title":"J. ACM"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: Ice: a robust framework for learning invariants. In: International Conference on Computer Aided Verification, pp. 69\u201387. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T.: Answer Set Solving in Practice. Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers (2012)","DOI":"10.1007\/978-3-031-01561-8"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1007\/978-3-319-89366-2_31","volume-title":"Foundations of Software Science and Computation Structures","author":"T Genet","year":"2018","unstructured":"Genet, T., Haudebourg, T., Jensen, T.: Verifying higher-order functions with tree automata. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 565\u2013582. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89366-2_31"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A.: Program verification with constrained horn clauses. In: CAV 2022. LNCS, vol. 13371, pp. 19\u201329. Springer (2022)","DOI":"10.1007\/978-3-031-13185-1_2"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Haudebourg, T., Genet, T., Jensen, T.: Regular language type inference with term rewriting. Proc. ACM Program. Lang. 4(ICFP), 1\u201329 (2020)","DOI":"10.1145\/3408994"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Hojjat, H., R\u00fcmmer, P.: The ELDARICA horn solver. In: FMCAD 2018, pp.\u00a01\u20137. IEEE (2018). https:\/\/github.com\/uuverifiers\/eldarica\/","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"724","DOI":"10.1007\/978-3-030-17184-1_26","volume-title":"Programming Languages and Systems","author":"M Journault","year":"2019","unstructured":"Journault, M., Min\u00e9, A., Ouadjaout, A.: An abstract domain for trees with numeric relations. In: Caires, L. (ed.) ESOP 2019. LNCS, vol. 11423, pp. 724\u2013751. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17184-1_26"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Kostyukov, Y., Mordvinov, D., Fedyukovich, G.: Beyond the elementary representations of program invariants over algebraic data types. In: Freund, S.N., Yahav, E. (eds.) PLDI 2021, pp. 451\u2013465. ACM (2021)","DOI":"10.1145\/3453483.3454055"},{"key":"10_CR17","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/s10817-006-9064-8","volume":"37","author":"S Limet","year":"2006","unstructured":"Limet, S., Salzer, G.: Tree tuple languages from the logic programming point of view. J. Autom. Reason. 37, 323\u2013349 (2006)","journal-title":"J. Autom. Reason."},{"key":"10_CR18","unstructured":"Losekoot, T., Genet, T., Jensen, T.: Automata-based verification of relational properties of functions over data structures. In: FSCD 2023, vol.\u00a0260. LIPIcs (2023)"},{"key":"10_CR19","unstructured":"Losekoot, T., Genet, T., Jensen, T.: Verification of programs with ADTs using Shallow Horn Clauses \u2013 extended version. Technical report, Univ Rennes, Inria, IRISA (2024). https:\/\/hal.inria.fr\/hal-04669706"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Matsumoto, Y., Kobayashi, N., Unno, H.: Automata-based abstraction for automated verification of higher-order tree-processing programs. In: Asian Symposium on Programming Languages and Systems, pp. 295\u2013312. Springer (2015)","DOI":"10.1007\/978-3-319-26529-2_16"},{"key":"10_CR21","unstructured":"Regular Invariant Generator (2021). https:\/\/github.com\/Columpio\/RInGen"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Shimoda, T., Kobayashi, N., Sakayori, K., Sato, R.: Symbolic automatic relations and their applications to SMT and CHC solving. In: International Static Analysis Symposium, pp. 405\u2013428. Springer (2021)","DOI":"10.1007\/978-3-030-88806-0_20"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Unno, H., Torii, S., Sakamoto, H.: Automating induction for solving horn clauses. In: International Conference on Computer Aided Verification, pp. 571\u2013591. Springer (2017)","DOI":"10.1007\/978-3-319-63390-9_30"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-74776-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T05:36:00Z","timestamp":1737351360000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-74776-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031747755","9783031747762"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-74776-2_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"21 January 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Static Analysis Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pasadena, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/2024.splashcon.org\/home\/sas-2024","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}