{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T00:25:14Z","timestamp":1760142314814,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":59,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986840"},{"type":"electronic","value":"9783031986857"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We address the problem of verifying automatically procedural programs manipulating parametric-size arrays of integers, encoded as a constrained Horn clauses solving problem. We propose a new algorithmic method for synthesizing loop invariants and procedure pre\/post-conditions represented as universally quantified first-order formulas constraining the array elements and program variables. We adopt a data-driven approach that extends the decision tree Horn-ICE framework to handle arrays. We provide a powerful learning technique based on reducing a complex classification problem of <jats:italic>vectors of integer arrays<\/jats:italic> to a simpler classification problem of <jats:italic>vectors of integers<\/jats:italic>. The obtained classifier is generalized to get universally quantified invariants and procedure pre\/post-conditions. We have implemented our method and shown its efficiency and competitiveness w.r.t. state-of-the-art tools on a significant benchmark.<\/jats:p>","DOI":"10.1007\/978-3-031-98685-7_16","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:32:57Z","timestamp":1753155177000},"page":"338-363","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Data-Driven Verification of\u00a0Procedural Programs with\u00a0Integer Arrays"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2060-3592","authenticated-orcid":false,"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2068-3729","authenticated-orcid":false,"given":"Wael-Amine","family":"Boutglay","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7982-0946","authenticated-orcid":false,"given":"Peter","family":"Habermehl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-28717-6_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F Alberti","year":"2012","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 46\u201361. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_7"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"679","DOI":"10.1007\/978-3-642-31424-7_49","volume-title":"Computer Aided Verification","author":"F Alberti","year":"2012","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: SAFARI: SMT-based abstraction for arrays with interpolants. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 679\u2013685. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_49"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-319-11936-6_2","volume-title":"Automated Technology for Verification and Analysis","author":"F Alberti","year":"2014","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Booster: an acceleration-based verification framework for array programs. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 18\u201323. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_2"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"Amilon, J., Esen, Z., Gurov, D., Lidstr\u00f6m, C., R\u00fcmmer, P.: Automatic program instrumentation for automatic verification. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, 17-22 July 2023, Proceedings, Part III. LNCS, vol. 13966, pp. 281\u2013304. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_14","DOI":"10.1007\/978-3-031-37709-9_14"},{"issue":"1","key":"16_CR5","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/s10009-002-0095-0","volume":"5","author":"T Ball","year":"2003","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking C programs. Int. J. Softw. Tools Technol. Transfer 5(1), 49\u201358 (2003). https:\/\/doi.org\/10.1007\/s10009-002-0095-0","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"16_CR6","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2016). https:\/\/smtlib.cs.uiowa.edu\/"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Barthe, G., Eilers, R., Georgiou, P., Gleiss, B., Kov\u00e1cs, L., Maffei, M.: Verifying Relational Properties using Trace Logic. In: Barrett, C.W., Yang, J. (eds.) 2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, 22-25 October 2019, pp. 170\u2013178. IEEE (2019)","DOI":"10.23919\/FMCAD.2019.8894277"},{"key":"16_CR8","doi-asserted-by":"publisher","unstructured":"Beyer, D.: State of the Art in Software Verification and Witness Validation: SV-COMP 2024. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, 6-11 April 2024, Proceedings, Part III. LNCS, vol. 14572, pp. 299\u2013329. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_15","DOI":"10.1007\/978-3-031-57256-2_15"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-69738-1_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 378\u2013394. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69738-1_27"},{"key":"16_CR10","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Boutglay, W., Habermehl, P.: Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, 7-10 August 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13371, pp. 282\u2013303. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_14","DOI":"10.1007\/978-3-031-13185-1_14"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Boutglay, W., Habermehl, P.: Data-driven verification of procedural programs with integer arrays. CoRR abs\/2505.15958 (2025)","DOI":"10.1007\/978-3-031-98685-7_16"},{"key":"16_CR13","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Boutglay, W.A., Habermehl, P.: Data-driven verification of procedural programs with integer arrays (Artifact) (2025). https:\/\/doi.org\/10.5281\/zenodo.15306371","DOI":"10.5281\/zenodo.15306371"},{"key":"16_CR14","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":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427\u2013442. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11609773_28"},{"key":"16_CR16","unstructured":"Braine, J.: The Data-abstraction framework: abstracting unbounded data-structures in Horn clauses, the case of arrays. (La M\u00e9thode Data-abstraction: UNE technique d\u2019abstraction de structures de donn\u00e9es non-born\u00e9es dans des clauses de Horn, le cas des tableaux). Ph.D. thesis, University of Lyon, France (2022)"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-030-88806-0_11","volume-title":"Static Analysis","author":"J Braine","year":"2021","unstructured":"Braine, J., Gonnord, L., Monniaux, D.: Data abstraction: a general framework to handle program verification of data structures. In: Dr\u0103goi, C., Mukherjee, S., Namjoshi, K. (eds.) SAS 2021. LNCS, vol. 12913, pp. 215\u2013235. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88806-0_11"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-030-45190-5_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Chakraborty","year":"2020","unstructured":"Chakraborty, S., Gupta, A., Unadkat, D.: Verifying array manipulating programs with full-program induction. In: TACAS 2020. LNCS, vol. 12078, pp. 22\u201339. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_2"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1007\/978-3-030-81688-9_42","volume-title":"Computer Aided Verification","author":"S Chakraborty","year":"2021","unstructured":"Chakraborty, S., Gupta, A., Unadkat, D.: Diffy: inductive reasoning of array programs using difference invariants. In: Silva, A., Leino, K. (eds.) CAV 2021. LNCS, vol. 12760, pp. 911\u2013935. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_42"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-030-02768-1_8","volume-title":"Programming Languages and Systems","author":"A Champion","year":"2018","unstructured":"Champion, A., Kobayashi, N., Sato, R.: HoIce: an ICE-based non-linear horn clause solver. In: Ryu, S. (ed.) APLAS 2018. LNCS, vol. 11275, pp. 146\u2013156. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02768-1_8"},{"issue":"3","key":"16_CR21","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/s10703-016-0257-4","volume":"49","author":"A Cimatti","year":"2016","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Infinite-state invariant checking with IC3 and predicate abstraction. Formal Methods Syst. Des. 49(3), 190\u2013218 (2016)","journal-title":"Formal Methods Syst. Des."},{"key":"16_CR22","unstructured":"Cimatti, A., Griggio, A., Tonetta, S.: The VMT-LIB language and tools. In: D\u00e9harbe, D., Hyv\u00e4rinen, A.E.J. (eds.) Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), Haifa, Israel, 11-12 August 2022. CEUR Workshop Proceedings, vol.\u00a03185, pp. 80\u201389. CEUR-WS.org (2022)"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A Parametric segmentation functor for fully automatic and scalable array content analysis. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pp. 105\u2013118. ACM (2011)","DOI":"10.1145\/1926385.1926399"},{"key":"16_CR25","doi-asserted-by":"publisher","unstructured":"De\u00a0Angelis, E., Vediramana\u00a0Krishnan, H.G.: Competition of Solvers for Constrained Horn Clauses (CHC-COMP 2023). In: TOOLympics Challenge 2023: Updates, Results, Successes of the Formal-Methods Competitions, pp. 38\u201351. Springer-Verlag (2024). https:\/\/doi.org\/10.1007\/978-3-031-67695-6_2","DOI":"10.1007\/978-3-031-67695-6_2"},{"key":"16_CR26","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: Bjesse, P., Slobodov\u00e1, A. (eds.) International Conference on Formal Methods in Computer-Aided Design, FMCAD 2011, Austin, TX, USA, October 30 - November 02, 2011, pp. 125\u2013134. FMCAD Inc. (2011)"},{"key":"16_CR27","unstructured":"Esen, Z., R\u00fcmmer, P.: Tricera: Verifying C programs using the theory of heaps. In: Griggio, A., Rungta, N. (eds.) 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, 17-21 October 2022, pp. 380\u2013391. IEEE (2022)"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Ezudheen, P., Neider, D., D\u2019Souza, D., Garg, P., Madhusudan, P.: Horn-ICE learning for synthesizing invariants and contracts. Proc. ACM Program. Lang. 2(OOPSLA), 131:1\u2013131:25 (2018)","DOI":"10.1145\/3276501"},{"key":"16_CR29","doi-asserted-by":"crossref","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.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018. pp.\u00a01\u20139. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603011"},{"key":"16_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-030-25540-4_14","volume-title":"Computer Aided Verification","author":"G Fedyukovich","year":"2019","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 259\u2013277. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_14"},{"issue":"4\u20135","key":"16_CR31","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1017\/S1471068415000204","volume":"15","author":"G Gange","year":"2015","unstructured":"Gange, G., Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.J.: Horn clauses as an intermediate representation for program analysis and transformation. Theory Pract. Log. Program. 15(4\u20135), 526\u2013542 (2015)","journal-title":"Theory Pract. Log. Program."},{"key":"16_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"813","DOI":"10.1007\/978-3-642-39799-8_57","volume-title":"Computer Aided Verification","author":"P Garg","year":"2013","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: Learning\u00a0universally\u00a0quantified\u00a0invariants of linear\u00a0data\u00a0structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 813\u2013829. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_57"},{"key":"16_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-08867-9_5","volume-title":"Computer Aided Verification","author":"P Garg","year":"2014","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: ICE:\u00a0A\u00a0robust\u00a0framework\u00a0for\u00a0learning\u00a0invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 69\u201387. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_5"},{"key":"16_CR34","doi-asserted-by":"crossref","unstructured":"Garg, P., Neider, D., Madhusudan, P., Roth, D.: Learning invariants using decision trees and implication counterexamples. In: Bod\u00edk, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20 - 22 January 2016, pp. 499\u2013512. ACM (2016)","DOI":"10.1145\/2837614.2837664"},{"key":"16_CR35","unstructured":"Georgiou, P., Gleiss, B., Kov\u00e1cs, L.: Trace logic for inductive loop reasoning. In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, 21-24 September 2020. pp. 255\u2013263. IEEE (2020)"},{"key":"16_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10"},{"key":"16_CR37","doi-asserted-by":"publisher","unstructured":"Griggio, A., Jon\u00e1s, M.: Kratos2: An SMT-Based Model Checker for Imperative Programs. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, 17-22 July 2023, Proceedings, Part III. LNCS, vol. 13966, pp. 423\u2013436. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_20","DOI":"10.1007\/978-3-031-37709-9_20"},{"key":"16_CR38","doi-asserted-by":"crossref","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, 7-12 January 2008, pp. 235\u2013246. ACM (2008)","DOI":"10.1145\/1328438.1328468"},{"key":"16_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-030-01090-4_15","volume-title":"Automated Technology for Verification and Analysis","author":"A Gurfinkel","year":"2018","unstructured":"Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 248\u2013266. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_15"},{"key":"16_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-03237-0_7","volume-title":"Static Analysis","author":"M Heizmann","year":"2009","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of Trace Abstraction. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 69\u201385. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03237-0_7"},{"key":"16_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/978-3-319-21690-4_40","volume-title":"Computer Aided Verification","author":"A Karbyshev","year":"2015","unstructured":"Karbyshev, A., Bj\u00f8rner, N., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 583\u2013602. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_40"},{"key":"16_CR42","doi-asserted-by":"crossref","unstructured":"Koenig, J.R., Padon, O., Immerman, N., Aiken, A.: First-order quantified separators. In: Donaldson, A.F., Torlak, E. (eds.) Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, 15-20 June 2020, pp. 703\u2013717. ACM (2020)","DOI":"10.1145\/3385412.3386018"},{"key":"16_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-08867-9_2","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2014","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17\u201334. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_2"},{"key":"16_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-642-17164-2_23","volume-title":"Programming Languages and Systems","author":"S Kong","year":"2010","unstructured":"Kong, S., Jung, Y., David, C., Wang, B.-Y., Yi, K.: Automatically inferring quantified loop invariants by algorithmic learning from simple templates. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 328\u2013343. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17164-2_23"},{"key":"16_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"16_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-319-89960-2_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Kumar","year":"2018","unstructured":"Kumar, S., Sanyal, A., Venkatesh, R., Shah, P.: Property checking array programs using loop shrinking. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 213\u2013231. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_12"},{"key":"16_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-540-24622-0_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"SK Lahiri","year":"2004","unstructured":"Lahiri, S.K., Bryant, R.E.: Constructing quantified invariants via predicate abstraction. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 267\u2013281. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_22"},{"key":"16_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-030-72016-2_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Mann","year":"2021","unstructured":"Mann, M., Irfan, A., Griggio, A., Padon, O., Barrett, C.: Counterexample-guided prophecy for model checking modulo the theory of arrays. In: TACAS 2021. LNCS, vol. 12651, pp. 113\u2013132. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_7"},{"key":"16_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123\u2013136. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_14"},{"issue":"1","key":"16_CR50","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. High. Order Symb. Comput. 19(1), 31\u2013100 (2006)","journal-title":"High. Order Symb. Comput."},{"key":"16_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-662-53413-7_18","volume-title":"Static Analysis","author":"D Monniaux","year":"2016","unstructured":"Monniaux, D., Gonnord, L.: Cell morphing: from array programs to array-free horn clauses. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 361\u2013382. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53413-7_18"},{"key":"16_CR52","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-540-71070-7_35","volume-title":"Automated Reasoning","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Deciding effectively propositional logic using DPLL and substitution sets. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 410\u2013425. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_35"},{"key":"16_CR53","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":"16_CR54","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Generalized, efficient array decision procedures. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA, pp. 45\u201352. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"16_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-030-25540-4_17","volume-title":"Computer Aided Verification","author":"S Padhi","year":"2019","unstructured":"Padhi, S., Millstein, T., Nori, A., Sharma, R.: Overfitting in synthesis: theory and practice. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 315\u2013334. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_17"},{"key":"16_CR56","doi-asserted-by":"crossref","unstructured":"Padhi, S., Sharma, R., Millstein, T.D.: Data-driven Precondition Inference with Learned Features. In: Krintz, C., Berger, E.D. (eds.) Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pp. 42\u201356. ACM (2016)","DOI":"10.1145\/2908080.2908099"},{"key":"16_CR57","doi-asserted-by":"publisher","unstructured":"Prabhu, S., D\u2019Souza, D., Chakraborty, S., Venkatesh, R., Fedyukovich, G.: Weakest Precondition Inference for Non-Deterministic Linear Array Programs. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, 6-11 April 2024, Proceedings, Part II. LNCS, vol. 14571, pp. 175\u2013195. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57249-4_9","DOI":"10.1007\/978-3-031-57249-4_9"},{"key":"16_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-030-03592-1_3","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"P Rajkhowa","year":"2018","unstructured":"Rajkhowa, P., Lin, F.: Extending VIAP to handle array programs. In: Piskac, R., R\u00fcmmer, P. (eds.) VSTTE 2018. LNCS, vol. 11294, pp. 38\u201349. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03592-1_3"},{"issue":"4","key":"16_CR59","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3686153","volume":"25","author":"G Redondi","year":"2024","unstructured":"Redondi, G., Cimatti, A., Griggio, A., McMillan, K.L.: Invariant checking for SMT-based systems with quantifiers. ACM Trans. Comput. Log. 25(4), 1\u201337 (2024)","journal-title":"ACM Trans. Comput. Log."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98685-7_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T08:55:02Z","timestamp":1760086502000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98685-7_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986840","9783031986857"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98685-7_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}