{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:52:34Z","timestamp":1781927554390,"version":"3.54.5"},"publisher-location":"Cham","reference-count":51,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031442445","type":"print"},{"value":"9783031442452","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[[2023]]},"DOI":"10.1007\/978-3-031-44245-2_13","type":"book-chapter","created":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T15:02:30Z","timestamp":1698073350000},"page":"259-285","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["ADCL: Acceleration Driven Clause Learning for\u00a0Constrained Horn Clauses"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0902-1994","authenticated-orcid":false,"given":"Florian","family":"Frohn","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0283-8520","authenticated-orcid":false,"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,10,24]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Artifact for \u201cADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses\u201d (2023). https:\/\/doi.org\/10.5281\/zenodo.8146788","DOI":"10.5281\/zenodo.8146788"},{"key":"13_CR2","unstructured":"Evaluation of \u201cADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses\u201d (2023). https:\/\/loat-developers.github.io\/adcl-evaluation. Source code of LoAT Source code of LoAT available at https:\/\/github.com\/loat-developers\/LoAT\/tree\/v0.4.0"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-031-13185-1_16","volume-title":"Computer Aided Verification","author":"L Alt","year":"2022","unstructured":"Alt, L., Blicha, M., Hyv\u00e4rinen, A.E.J., Sharygina, N.: SolCMC: Solidity compiler\u2019s model checker. In: Shoham, S., Vizel, Y. (eds.) CAV 2022. LNCS, vol. 13371, pp. 325\u2013338. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_16"},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Bagnara, R., Pescetti, A., Zaccagnini, A., Zaffanella, E.: PURRS: towards computer algebra support for fully automatic worst-case complexity analysis. CoRR abs\/cs\/0512056 (2005). https:\/\/doi.org\/10.48550\/arXiv.cs\/0512056","DOI":"10.48550\/arXiv.cs\/0512056"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/11562948_35","volume-title":"Automated Technology for Verification and Analysis","author":"S Bardin","year":"2005","unstructured":"Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 474\u2013488. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11562948_35"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Biere, A.: Bounded model checking. In: Handbook of Satisfiability - Second Edition. Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 739\u2013764. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA201002","DOI":"10.3233\/FAIA201002"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1007\/978-3-030-99524-9_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Blicha","year":"2022","unstructured":"Blicha, M., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Transition power abstractions for deep counterexample detection. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 524\u2013542. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_29"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-642-00768-2_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Bozga","year":"2009","unstructured":"Bozga, M., G\u00eerlea, C., Iosif, R.: Iterating octagons. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 337\u2013351. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_29"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-14295-6_23","volume-title":"Computer Aided Verification","author":"M Bozga","year":"2010","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 227\u2013242. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_23"},{"key":"13_CR10","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Relational analysis of integer programs. Technical report TR-2012-10, VERIMAG (2012). https:\/\/www-verimag.imag.fr\/TR\/TR-2012-10.pdf"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Calzavara, S., Grishchenko, I., Maffei, M.: HornDroid: practical and sound static analysis of Android applications by SMT solving. In: EuroS &P 2016, pp. 47\u201362. IEEE (2016). https:\/\/doi.org\/10.1109\/EuroSP.2016.16","DOI":"10.1109\/EuroSP.2016.16"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-540-78800-3_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Caniart","year":"2008","unstructured":"Caniart, N., Fleury, E., Leroux, J., Zeitoun, M.: Accelerating interpolation-based model-checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 428\u2013442. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_32"},{"key":"13_CR14","unstructured":"CHC Competition. https:\/\/chc-comp.github.io"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Chen, Y., Kov\u00e1cs, L., Robillard, S.: Theory-specific reasoning about loops with arrays using Vampire. In: Kov\u00e1cs, L., Voronkov, A. (eds.) Vampire@IJCAR 2016, pp. 16\u201332. EPiC 44 (2016). https:\/\/doi.org\/10.29007\/qk21","DOI":"10.29007\/qk21"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/BFb0028751","volume-title":"Computer Aided Verification","author":"H Comon","year":"1998","unstructured":"Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and Presburger arithmetic. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 268\u2013279. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028751"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"Dietsch, D., Heizmann, M., Hoenicke, J., Nutz, A., Podelski, A.: Ultimate TreeAutomizer (CHC-COMP tool description). In: De Angelis, E., Fedyukovich, G., Tzevelekos, N., Ulbrich, M. (eds.) HCVS\/PERR@ETAPS 2019, pp. 42\u201347. EPTCS 296 (2019). https:\/\/doi.org\/10.4204\/EPTCS.296.7","DOI":"10.4204\/EPTCS.296.7"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-030-94583-1_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G Ernst","year":"2022","unstructured":"Ernst, G.: Loop verification with invariants and contracts. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 69\u201392. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_4"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Solving constrained Horn clauses using syntax and data. In: Bj\u00f8rner, N.S., Gurfinkel, A. (eds.) FMCAD 2018, pp. 1\u20139 (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603011","DOI":"10.23919\/FMCAD.2018.8603011"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-36206-1_14","volume-title":"FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science","author":"A Finkel","year":"2002","unstructured":"Finkel, A., Leroux, J.: How to compose Presburger-accelerations: applications to broadcast protocols. In: Agrawal, M., Seth, A. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 145\u2013156. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36206-1_14"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Proving non-termination via loop acceleration. In: Barrett, C.W., Yang, J. (eds.) FMCAD 2019, pp. 221\u2013230 (2019). https:\/\/doi.org\/10.23919\/FMCAD.2019.8894271","DOI":"10.23919\/FMCAD.2019.8894271"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-030-45190-5_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Frohn","year":"2020","unstructured":"Frohn, F.: A calculus for modular loop acceleration. In: Biere, A., Parker, D. (eds.) TACAS 2020. LNCS, vol. 12078, pp. 58\u201376. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_4"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"712","DOI":"10.1007\/978-3-031-10769-6_41","volume-title":"Automated Reasoning","author":"F Frohn","year":"2022","unstructured":"Frohn, F., Giesl, J.: Proving non-termination and lower runtime bounds with LoAT (system description). In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 712\u2013722. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_41"},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Proving non-termination by acceleration driven clause learning (short paper). In: Pientka, B., Tinelli, C. (eds.) CADE 2023. LNCS, vol 14132, pp. 220\u2013233. Springer, Cham (2023). Full version appeared in CoRR abs\/2304.10166. https:\/\/doi.org\/10.48550\/arXiv.2304.10166","DOI":"10.48550\/arXiv.2304.10166"},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: ADCL: acceleration driven clause learning for constrained Horn clauses. CoRR abs\/2303.01827 (2023). https:\/\/doi.org\/10.48550\/arXiv.2303.01827","DOI":"10.48550\/arXiv.2303.01827"},{"issue":"5","key":"13_CR27","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1007\/s10009-016-0420-7","volume":"19","author":"P Ganty","year":"2016","unstructured":"Ganty, P., Iosif, R., Kone\u010dn\u00fd, F.: Underapproximation of procedure summaries for integer programs. Int. J. Softw. Tools Technol. Transfer 19(5), 565\u2013584 (2016). https:\/\/doi.org\/10.1007\/s10009-016-0420-7","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"13_CR28","unstructured":"Gomes, C.P., Selman, B., Kautz, H.A.: Boosting combinatorial search through randomization. In: Mostow, J., Rich, C. (eds.) AAAI 1998, pp. 431\u2013437 (1998). https:\/\/www.cs.cornell.edu\/gomes\/pdf\/1998_gomes_aaai_iaai_boosting.pdf"},{"key":"13_CR29","doi-asserted-by":"publisher","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Vitek, J., Lin, H., Tip, F. (eds.) PLDI 2012, pp. 405\u2013416 (2012). https:\/\/doi.org\/10.1145\/2254064.2254112","DOI":"10.1145\/2254064.2254112"},{"key":"13_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"key":"13_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-11439-2_9","volume-title":"Reachability Problems","author":"C Haase","year":"2014","unstructured":"Haase, C., Halfon, S.: Integer vector addition systems with states. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 112\u2013124. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11439-2_9"},{"key":"13_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-16242-8_25","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"TA Henzinger","year":"2010","unstructured":"Henzinger, T.A., Hottelier, T., Kov\u00e1cs, L., Rybalchenko, A.: Aligators for arrays (tool paper). In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 348\u2013356. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16242-8_25"},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157\u2013171. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_13"},{"key":"13_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-33386-6_16","volume-title":"Automated Technology for Verification and Analysis","author":"H Hojjat","year":"2012","unstructured":"Hojjat, H., Iosif, R., Kone\u010dn\u00fd, F., Kuncak, V., R\u00fcmmer, P.: Accelerating interpolants. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 187\u2013202. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_16"},{"key":"13_CR35","doi-asserted-by":"publisher","unstructured":"Hojjat, H., R\u00fcmmer, P.: The Eldarica Horn solver. In: Bj\u00f8rner, N.S., Gurfinkel, A. (eds.) FMCAD 2018, pp. 1\u20137 (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"13_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-319-41528-4_19","volume-title":"Computer Aided Verification","author":"T Kahsai","year":"2016","unstructured":"Kahsai, T., R\u00fcmmer, P., Sanchez, H., Sch\u00e4f, M.: JayHorn: a framework for verifying Java programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 352\u2013358. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_19"},{"issue":"3","key":"13_CR37","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.: SMT-based model checking for recursive programs. Formal Methods Syst. Design 48(3), 175\u2013205 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0249-4","journal-title":"Formal Methods Syst. Design"},{"key":"13_CR38","doi-asserted-by":"publisher","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 (2021). https:\/\/doi.org\/10.1145\/3453483.3454055","DOI":"10.1145\/3453483.3454055"},{"key":"13_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-642-00593-0_33","volume-title":"Fundamental Approaches to Software Engineering","author":"L Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 470\u2013485. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00593-0_33"},{"issue":"1","key":"13_CR40","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/s10703-015-0228-1","volume":"47","author":"D Kroening","year":"2015","unstructured":"Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in C programs for fast counterexample detection. Formal Methods Syst. Design 47(1), 75\u201392 (2015). https:\/\/doi.org\/10.1007\/s10703-015-0228-1","journal-title":"Formal Methods Syst. Design"},{"key":"13_CR41","unstructured":"libFAUDES Library. https:\/\/fgdes.tf.fau.de\/faudes\/index.html"},{"issue":"4","key":"13_CR42","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0020-0190(93)90029-9","volume":"47","author":"M Luby","year":"1993","unstructured":"Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of Las Vegas algorithms. Inf. Process. Lett. 47(4), 173\u2013180 (1993). https:\/\/doi.org\/10.1016\/0020-0190(93)90029-9","journal-title":"Inf. Process. Lett."},{"key":"13_CR43","doi-asserted-by":"publisher","unstructured":"Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for Rust programs. ACM Trans. Program. Lang. Syst. 43(4), 15:1\u201315:54 (2021). https:\/\/doi.org\/10.1145\/3462205","DOI":"10.1145\/3462205"},{"key":"13_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"13_CR45","unstructured":"OEIS Foundation Inc.: Thue-Morse sequence. The On-Line Encyclopedia of Integer Sequences. https:\/\/oeis.org\/A010060"},{"key":"13_CR46","unstructured":"OEIS Foundation Inc.: First differences of Thue-Morse sequence. The On-Line Encyclopedia of Integer Sequences (1999). https:\/\/oeis.org\/A029883"},{"key":"13_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-23702-7_19","volume-title":"Static Analysis","author":"P Schrammel","year":"2011","unstructured":"Schrammel, P., Jeannet, B.: Logico-numerical abstract acceleration and application to the verification of data-flow programs. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 233\u2013248. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23702-7_19"},{"key":"13_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-030-25543-5_7","volume-title":"Computer Aided Verification","author":"J Silverman","year":"2019","unstructured":"Silverman, J., Kincaid, Z.: Loop summarization with rational vector addition systems. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 97\u2013115. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_7"},{"key":"13_CR49","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-08587-6_28","volume-title":"Automated Reasoning","author":"A Stump","year":"2014","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 367\u2013373. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28"},{"key":"13_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-030-94583-1_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Wesley","year":"2022","unstructured":"Wesley, S., Christakis, M., Navas, J.A., Trefler, R., W\u00fcstholz, V., Gurfinkel, A.: Verifying Solidity smart contracts via communication abstraction in SmartACE. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 425\u2013449. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_21"},{"key":"13_CR51","doi-asserted-by":"publisher","unstructured":"Zhu, H., Magill, S., Jagannathan, S.: A data-driven CHC solver. In: Foster, J.S., Grossman, D. (eds.) PLDI 2018, pp. 707\u2013721 (2018). https:\/\/doi.org\/10.1145\/3192366.3192416","DOI":"10.1145\/3192366.3192416"}],"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-44245-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,8]],"date-time":"2024-02-08T08:14:44Z","timestamp":1707380084000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-44245-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031442445","9783031442452"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-44245-2_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"24 October 2023","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":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 October 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/sas-2023","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}