{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T16:07:59Z","timestamp":1779034079599,"version":"3.51.4"},"publisher-location":"Cham","reference-count":61,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262035","type":"print"},{"value":"9783032262042","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Function contract generation is a classical problem in program analysis that targets the automated analysis of functions in a program with multiple procedures. The problem is fundamental in interprocedural analysis where properties of functions are first obtained via the generation of function contracts and then the generated contracts are used as building blocks to analyze the whole program. Typical objectives in function contract generation include pre-\/post-conditions and assigns information (that specifies the modification information over program variables and memory segments during function execution). In programs with array manipulations, a crucial point in function contract generation is the treatment of array segments that imposes challenges in inferring invariants and assigns information over such segments. To address this challenge, we propose a novel symbolic execution framework that carries invariants and assigns information over contiguous segments of arrays. We implement our framework as a prototype within LLVM, and further integrate our prototype with the ANSI\/ISO C Specification Language (ACSL) assertion format and the Frama-C software verification platform. Experimental evaluation over a variety of benchmarks from the literature and functions from realistic libraries shows that our framework is capable of handling array manipulating functions that indeed involve the carry of array information and are beyond existing approaches.<\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_21","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:50:45Z","timestamp":1779033045000},"page":"397-418","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Array-Carrying Symbolic Execution for\u00a0Function Contract Generation"],"prefix":"10.1007","author":[{"given":"Weijie","family":"Lu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jingyu","family":"Ke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7947-3446","authenticated-orcid":false,"given":"Hongfei","family":"Fu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhouyue","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yi","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guoqiang","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Haokun","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"21_CR1","unstructured":"Alur, R., Fisman, D., Padhi, S., Singh, R., Udupa, A.: Sygus-comp 2018: results and analysis (2019). https:\/\/arxiv.org\/abs\/1904.07146"},{"key":"21_CR2","unstructured":"Amilon, J.: Automated inference of ACSL function contracts using Tricera (2021)"},{"key":"21_CR3","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. Lecture Notes in Computer Science, 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"},{"key":"21_CR4","doi-asserted-by":"publisher","unstructured":"Asadi, A., Chatterjee, K., Fu, H., Goharshady, A.K., Mahdavi, M.: Polynomial reachability witnesses via stellens\u00e4tze. In: Freund, S.N., Yahav, E. (eds.) PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, 20-25 June 2021, pp. 772\u2013787. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454076","DOI":"10.1145\/3453483.3454076"},{"key":"21_CR5","unstructured":"Baudin, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C specification. https:\/\/frama-c.com\/html\/acsl.html (2021)"},{"key":"21_CR6","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-030-11245-5_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Boutonnet","year":"2019","unstructured":"Boutonnet, R., Halbwachs, N.: Disjunctive relational abstract interpretation for interprocedural program analysis. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 136\u2013159. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_7"},{"key":"21_CR8","unstructured":"Cadar, C., Dunbar, D., Engler, D.R., et\u00a0al.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI. vol.\u00a08, pp. 209\u2013224 (2008)"},{"key":"21_CR9","unstructured":"CEA LIST: Frama-C: a software analysis platform (2024). https:\/\/frama-c.com"},{"key":"21_CR10","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K., Goharshady, E.K.: Polynomial invariant generation for non-deterministic recursive programs. 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. 672\u2013687. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385969","DOI":"10.1145\/3385412.3385969"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"MA Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420\u2013432. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_39"},{"issue":"4","key":"21_CR12","doi-asserted-by":"publisher","first-page":"957","DOI":"10.1109\/TSE.2011.59","volume":"38","author":"L Cordeiro","year":"2011","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-c software. IEEE Trans. Softw. Eng. 38(4), 957\u2013974 (2011)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"21_CR13","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: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-35873-9_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Cousot","year":"2013","unstructured":"Cousot, P., Cousot, R., F\u00e4hndrich, M., Logozzo, F.: Automatic inference of necessary preconditions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 128\u2013148. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_10"},{"key":"21_CR15","doi-asserted-by":"publisher","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, 26-28 January 2011, pp. 105\u2013118. ACM (2011). https:\/\/doi.org\/10.1145\/1926385.1926399","DOI":"10.1145\/1926385.1926399"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: Precondition inference from intermittent assertions and application to contracts on collections. In: International Workshop on Verification, Model Checking, and Abstract Interpretation, pp. 150\u2013168. Springer (2011)","DOI":"10.1007\/978-3-642-18275-4_12"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233\u2013247. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16"},{"issue":"10","key":"21_CR18","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1145\/2544173.2509511","volume":"48","author":"I Dillig","year":"2013","unstructured":"Dillig, I., Dillig, T., Li, B., McMillan, K.: Inductive invariant generation via abductive inference. SIGPLAN Not. 48(10), 443\u2013456 (2013). https:\/\/doi.org\/10.1145\/2544173.2509511","journal-title":"SIGPLAN Not."},{"key":"21_CR19","doi-asserted-by":"publisher","unstructured":"Esen, Z., R\u00fcmmer, P.: TriCera: verifying C programs using the theory of heaps. In: Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design (FMCAD 2022), pp. 360\u2013367. TU Wien Academic Press (2022). 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":"21_CR20","doi-asserted-by":"crossref","unstructured":"Garcia-Contreras, I., Gurfinkel, A., Navas, J.A.: Efficient modular SMT-based model checking of pointer programs. In: International Static Analysis Symposium, pp. 227\u2013246. Springer (2022)","DOI":"10.1007\/978-3-031-22308-2_11"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT model checking of array-based systems. In: International Joint Conference on Automated Reasoning, pp. 67\u201382. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_6"},{"key":"21_CR22","doi-asserted-by":"publisher","unstructured":"Gopan, D., Reps, T.W., Sagiv, S.: A framework for numeric analysis of array operations. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, 12-14 January 2005, pp. 338\u2013350. ACM (2005). https:\/\/doi.org\/10.1145\/1040305.1040333","DOI":"10.1145\/1040305.1040333"},{"key":"21_CR23","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., Pasareanu, C.S. (eds.) Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, 18-24 July 2015, Proceedings, Part I. Lecture Notes in Computer Science, vol.\u00a09206, pp. 343\u2013361. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Hojjat, H., R\u00fcmmer, P.: The eldarica horn solver. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pp.\u00a01\u20137. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"21_CR25","unstructured":"Hol\u00edk, L., Peringer, P., Rogalewicz, A., \u0160okov\u00e1, V., Vojnar, T., Zuleger, F.: Low-level Bi-abduction. In: 36th European Conference on Object-Oriented Programming (ECOOP 2022). LIPIcs (2022). arXiv:2205.02590"},{"key":"21_CR26","doi-asserted-by":"publisher","unstructured":"Ji, Y., Fu, H., Fang, B., Chen, H.: Affine loop invariant generation via matrix algebra. 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. 257\u2013281. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_13","DOI":"10.1007\/978-3-031-13185-1_13"},{"key":"21_CR27","unstructured":"Kapus, T., Cadar, C.: A segmented memory model for symbolic execution. In: ESEC\/FSE, pp. 1002\u20131012. ACM (2019)"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Ke, J., Fu, H., Liu, H., Sun, Z., Chen, L., Li, G.: Affine disjunctive invariant generation with Farkas\u2019 lemma. In: International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 187\u2013213. Springer (2025)","DOI":"10.1007\/978-3-031-82700-6_9"},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"Kincaid, Z., Cyphert, J., Breck, J., Reps, T.: Non-linear reasoning for invariant synthesis. In: Proceedings of the ACM on Programming Languages, vol. 2(POPL), pp. 1\u201333 (2017)","DOI":"10.1145\/3158142"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"King, D., Koutavas, V., Kov\u00e1cs, L.: LLM-Based generation of weakest preconditions and precise array invariants. In: Proceedings of the 13th IEEE\/ACM International Conference on Formal Methods in Software Engineering, (FormaliSE@ICSE\u201925), pp.\u00a01\u20135. IEEE (2025)","DOI":"10.1109\/FormaliSE66629.2025.00016"},{"issue":"3","key":"21_CR31","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-c: a software analysis perspective. Formal Aspects Comput. 27(3), 573\u2013609 (2015)","journal-title":"Formal Aspects Comput."},{"issue":"3","key":"21_CR32","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. Des. 48(3), 175\u2013205 (2016). https:\/\/doi.org\/10.1007\/S10703-016-0249-4","journal-title":"Formal Methods Syst. Des."},{"key":"21_CR33","unstructured":"Kremenek, T.: Finding software bugs with the clang static analyzer. Apple Inc 8, 2008 (2008)"},{"key":"21_CR34","doi-asserted-by":"crossref","unstructured":"Krishna, M., Gaur, B., Verma, A., Jalote, P.: Using LLMs in software requirements specifications: an empirical evaluation. In: Preceedings of the 32nd IEEE International Requirements Engineering Conference (RE\u201924), pp. 475\u2013483. IEEE (2024)","DOI":"10.1109\/RE59067.2024.00056"},{"key":"21_CR35","doi-asserted-by":"publisher","unstructured":"Larraz, D., Rodr\u00edguez-Carbonell, E., Rubio, A.: SMT-based array invariant generation. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, 20-22 January 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a07737, pp. 169\u2013188. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_12","DOI":"10.1007\/978-3-642-35873-9_12"},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.: LLVM: A compilation framework for lifelong program analysis & transformation. In: Proceedings of the International Symposium on Code Generation and Optimization (CGO\u201904), pp. 75\u201386. IEEE Computer Society (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"21_CR37","doi-asserted-by":"crossref","unstructured":"Le-Cong, T., Le, B., Murray, T.: Can LLMs reason about program semantics? a comprehensive evaluation of LLMs on formal specification inference. In: Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (ACL\u201925), pp. 21991\u201322014. Association for Computational Linguistics (2025)","DOI":"10.18653\/v1\/2025.acl-long.1068"},{"key":"21_CR38","doi-asserted-by":"crossref","unstructured":"Li, B., Tang, Z., Zhai, J., Zhao, J.: Automatic invariant synthesis for arrays in simple programs. In: 2016 IEEE International Conference on Software Quality, Reliability and Security (QRS), pp. 108\u2013119. IEEE (2016)","DOI":"10.1109\/QRS.2016.23"},{"key":"21_CR39","doi-asserted-by":"publisher","unstructured":"Li, Y., Fu, H., Long, H., Li, G.: Constraint based invariant generation with modular operations. In: Bourke, T., Chen, L., Goharshady, A.K. (eds.) Dependable Software Engineering. Theories, Tools, and Applications - 10th International Symposium, SETTA 2024, Hong Kong, China, 26-28 November 2024, Proceedings. Lecture Notes in Computer Science, vol. 15469, pp. 64\u201384. Springer (2024). https:\/\/doi.org\/10.1007\/978-981-96-0602-3_4","DOI":"10.1007\/978-981-96-0602-3_4"},{"key":"21_CR40","unstructured":"Liu, C., Wu, X., Feng, Y., Cao, Q., Yan, J.: Towards general loop invariant generation: a benchmark of programs with memory manipulation. In: Annual Conference on Neural Information Processing Systems( NeurIPS\u201924). Advances in Neural Information Processing Systems, vol.\u00a038 (2024)"},{"issue":"OOPSLA2","key":"21_CR41","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1145\/3563295","volume":"6","author":"H Liu","year":"2022","unstructured":"Liu, H., Fu, H., Yu, Z., Song, J., Li, G.: Scalable linear invariant generation with Farkas\u2019 lemma. Proc. ACM Program. Lang. 6(OOPSLA2), 204\u2013232 (2022)","journal-title":"Proc. ACM Program. Lang."},{"key":"21_CR42","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2025.103387","volume":"248","author":"R Liu","year":"2026","unstructured":"Liu, R., Chen, M., Wu, L., Ke, J., Li, G.: Enhancing automated loop invariant generation for complex programs with large language models. Sci. Comput. Program. 248, 103387 (2026)","journal-title":"Sci. Comput. Program."},{"key":"21_CR43","unstructured":"Lu, W., Ke, J., Fu, H., Sun, Z., Zhou, Y., Li, G., Li, H.: Array-carrying symbolic execution for function contract generation (2026). https:\/\/arxiv.org\/abs\/2602.23216"},{"key":"21_CR44","doi-asserted-by":"crossref","unstructured":"Ma, L., Liu, S., Li, Y., Xie, X., Bu, L.: SpecGen: automated generation of formal program specifications via large language models. In: Proceedings of the 47th IEEE\/ACM International Conference on Software Engineering, (ICSE\u201925), pp. 16\u201328. IEEE (2025)","DOI":"10.1109\/ICSE55347.2025.00129"},{"key":"21_CR45","doi-asserted-by":"publisher","unstructured":"Maksimovi\u0107, P., Ayoun, S.\u00c9., Santos, J.F., Gardner, P.: Gillian, part II: Real-world verification for javascript and c. In: Computer Aided Verification (CAV 2021), Proceedings, Part II. Lecture Notes in Computer Science, vol. 12760, pp. 827\u2013850. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_38","DOI":"10.1007\/978-3-030-81688-9_38"},{"key":"21_CR46","doi-asserted-by":"publisher","unstructured":"McCloskey, B., Reps, T.W., Sagiv, M.: Statically inferring complex heap, array, and numeric invariants. In: Cousot, R., Martel, M. (eds.) Static Analysis - 17th International Symposium, SAS 2010, Perpignan, France, 14-16 September 2010. Proceedings. Lecture Notes in Computer Science, vol.\u00a06337, pp. 71\u201399. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_6","DOI":"10.1007\/978-3-642-15769-1_6"},{"key":"21_CR47","unstructured":"openHiTLS Project: openhitls. https:\/\/github.com\/openHiTLS\/openHiTLS (2023), cryptography and TLS library, Accessed 27 Nov 2025"},{"key":"21_CR48","unstructured":"Pei, K., Bieber, D., Shi, K., Sutton, C., Yin, P.: Can large language models reason about program invariants? In: International Conference on Machine Learning (ICML\u201923). Proceedings of Machine Learning Research, vol.\u00a0202, pp. 27496\u201327520. PMLR (2023)"},{"key":"21_CR49","doi-asserted-by":"crossref","unstructured":"Pirzada, M.A.A., Reger, G., Bhayat, A., Cordeiro, L.C.: LLM-generated invariants for bounded model checking without loop unrolling. In: Proceedings of the 39th IEEE\/ACM International Conference on Automated Software Engineering (ASE\u201924), pp. 1395\u20131407. ACM (2024)","DOI":"10.1145\/3691620.3695512"},{"key":"21_CR50","unstructured":"Ramos, D.A., Engler, D.: Under-constrained symbolic execution: correctness checking for real code. In: USENIX Security (2015)"},{"key":"21_CR51","unstructured":"RSE-Verification: Auto-Deduct Toolchain: automated formal verification toolchain. https:\/\/github.com\/rse-verification\/auto-deduct-toolchain (2025), Accessed 30 Nov 2025 cc41d5a602ab58dc997662530a8aa23efac36633"},{"key":"21_CR52","unstructured":"RSE-Verification: Interface Specification Propagator (ISP): Frama-c plugin. https:\/\/github.com\/rse-verification\/interface-specification-propagator (2025), Accessed 30 Nov 2025"},{"key":"21_CR53","unstructured":"RSE-Verification: Saida: a frama-c plugin for ACSL contract verification. https:\/\/github.com\/rse-verification\/saida (2025), Accessed 30 Nov 2025"},{"key":"21_CR54","unstructured":"RSE-Verification: Tricera: A model checker for c programs (RSE-verification fork). https:\/\/github.com\/rse-verification\/tricera (2025), Accessed 30 Nov 2025"},{"key":"21_CR55","doi-asserted-by":"publisher","unstructured":"Santos, J.F., Maksimovi\u0107, P., Ayoun, S.\u00c9., Gardner, P.: Gillian, part I: a multi-language platform for symbolic execution. In: Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2020), pp. 927\u2013942. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3386014","DOI":"10.1145\/3385412.3386014"},{"key":"21_CR56","unstructured":"The LLVM Compiler Infrastructure: LLVM compiler infrastructure (2025). https:\/\/llvm.org, release 19.1.7"},{"key":"21_CR57","unstructured":"Uppsala University (uuverifiers): TriCera: a model checker for C programs. https:\/\/github.com\/uuverifiers\/tricera (2025), Accessed 30 Nov 2025"},{"issue":"OOPSLA1","key":"21_CR58","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/3586028","volume":"7","author":"C Wang","year":"2023","unstructured":"Wang, C., Lin, F.: Solving conditional linear recurrences for program verification: the periodic case. Proc. ACM Program. Lang. 7(OOPSLA1), 28\u201355 (2023). https:\/\/doi.org\/10.1145\/3586028","journal-title":"Proc. ACM Program. Lang."},{"key":"21_CR59","doi-asserted-by":"crossref","unstructured":"Wen, C., et al.: Enchanting program specification synthesis by large language models using static analysis and program verification. In: Proceedings of the 36th International Conference on Computer Aided Verification (CAV\u201924) Part II. Lecture Notes in Computer Science, vol. 14682, pp. 302\u2013328. Springer (2024)","DOI":"10.1007\/978-3-031-65630-9_16"},{"key":"21_CR60","doi-asserted-by":"crossref","unstructured":"Xie, D., et al.: How effective are large language models in generating software specifications? In: Proceedings of the 32nd IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER\u201925), pp. 1\u201312. IEEE (2025)","DOI":"10.1109\/SANER64311.2025.00014"},{"key":"21_CR61","doi-asserted-by":"publisher","unstructured":"Yao, P., Ke, J., Sun, J., Fu, H., Wu, R., Ren, K.: Demystifying template-based invariant generation for bit-vector programs. In: 38th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2023, Luxembourg, 11-15 September 2023, pp. 673\u2013685. IEEE (2023). https:\/\/doi.org\/10.1109\/ASE56229.2023.00069","DOI":"10.1109\/ASE56229.2023.00069"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26204-2_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:50:49Z","timestamp":1779033049000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}