{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:37Z","timestamp":1775873677764,"version":"3.50.1"},"publisher-location":"Cham","reference-count":69,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656293","type":"print"},{"value":"9783031656309","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T00:00:00Z","timestamp":1721865600000},"content-version":"vor","delay-in-days":206,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Formal verification provides a rigorous and systematic approach to ensure the correctness and reliability of software systems. Yet, constructing specifications for the full proof relies on domain expertise and non-trivial manpower. In view of such needs, an automated approach for specification synthesis is desired. While existing automated approaches are limited in their versatility,<jats:italic>i.e.<\/jats:italic>, they either focus only on synthesizing loop invariants for numerical programs, or are tailored for specific types of programs or invariants. Programs involving multiple complicated data types (<jats:italic>e.g.<\/jats:italic>, arrays, pointers) and code structures (<jats:italic>e.g.<\/jats:italic>, nested loops, function calls) are often beyond their capabilities. To help bridge this gap, we present<jats:sc>AutoSpec<\/jats:sc>, an automated approach to synthesize specifications for automated program verification. It overcomes the shortcomings of existing work in specification versatility, synthesizing satisfiable and adequate specifications for full proof. It is driven by static analysis and program verification, and is empowered by large language models (LLMs).<jats:sc>AutoSpec<\/jats:sc>addresses the practical challenges in three ways: (1) driving<jats:sc>AutoSpec<\/jats:sc>by static analysis and program verification, LLMs serve as generators to generate candidate specifications, (2) programs are decomposed to direct the attention of LLMs, and (3) candidate specifications are validated in each round to avoid error accumulation during the interaction with LLMs. In this way,<jats:sc>AutoSpec<\/jats:sc>can incrementally and iteratively generate satisfiable and adequate specifications. The evaluation shows its effectiveness and usefulness, as it outperforms existing works by successfully verifying 79% of programs through automatic specification synthesis, a significant improvement of 1.592x. It can also be successfully applied to verify the programs in a real-world X509-parser project.<\/jats:p>","DOI":"10.1007\/978-3-031-65630-9_16","type":"book-chapter","created":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T22:01:56Z","timestamp":1721858516000},"page":"302-328","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":32,"title":["Enchanting Program Specification Synthesis by\u00a0Large Language Models Using Static Analysis and\u00a0Program Verification"],"prefix":"10.1007","author":[{"given":"Cheng","family":"Wen","sequence":"first","affiliation":[]},{"given":"Jialun","family":"Cao","sequence":"additional","affiliation":[]},{"given":"Jie","family":"Su","sequence":"additional","affiliation":[]},{"given":"Zhiwu","family":"Xu","sequence":"additional","affiliation":[]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[]},{"given":"Mengda","family":"He","sequence":"additional","affiliation":[]},{"given":"Haokun","family":"Li","sequence":"additional","affiliation":[]},{"given":"Shing-Chi","family":"Cheung","sequence":"additional","affiliation":[]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,25]]},"reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-319-91908-9_18","volume-title":"Computing and Software Science","author":"R H\u00e4hnle","year":"2019","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: from pen-and-paper proofs to industrial tools. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 345\u2013373. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18"},{"key":"16_CR2","first-page":"1","volume":"31","author":"X Si","year":"2018","unstructured":"Si, X., Dai, H., Raghothaman, M., Naik, M., Song, L.: Learning loop invariants for program verification. Adv. Neural Inf. Process. Syst. 31, 1\u201312 (2018)","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"16_CR3","unstructured":"Ebalard, A., Mouy, P., Benadjila, R.: Journey to a rte-free x. 509 parser. In: Symposium sur la s\u00e9curit\u00e9 des technologies de l\u2019information et des communications (SSTIC 2019) (2019)"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-030-03421-4_15","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"D Efremov","year":"2018","unstructured":"Efremov, D., Mandrykin, M., Khoroshilov, A.: Deductive verification of unmodified linux kernel library functions. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 216\u2013234. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_15"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Dordowsky, F.: An experimental study using acsl and frama-c to formulate and verify low-level requirements from a do-178c compliant avionics project. arXiv preprint arXiv:1508.03894 (2015)","DOI":"10.4204\/EPTCS.187.3"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-319-19458-5_2","volume-title":"Formal Methods for Industrial Critical Systems","author":"A Blanchard","year":"2015","unstructured":"Blanchard, A., Kosmatov, N., Lemerre, M., Loulergue, F.: A case study on formal verification of the anaxagoros hypervisor paging system with frama-C. In: N\u00fa\u00f1ez, M., G\u00fcdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 15\u201330. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19458-5_2"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-319-09099-3_12","volume-title":"Tests and Proofs","author":"N Kosmatov","year":"2014","unstructured":"Kosmatov, N., Lemerre, M., Alec, C.: A case study on verification of a cloud hypervisor by proof and structural testing. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 158\u2013164. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09099-3_12"},{"issue":"10","key":"16_CR8","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. Acm Sigplan Not. 48(10), 443\u2013456 (2013)","journal-title":"Acm Sigplan Not."},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Lin, Y., et al.: Inferring loop invariants for multi-path loops. In: 2021 International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 63\u201370. IEEE (2021)","DOI":"10.1109\/TASE52547.2021.00030"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Yu, S., Wang, T., Wang, J.: Loop invariant inference through smt solving enhanced reinforcement learning. In: Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 175\u2013187 (2023)","DOI":"10.1145\/3597926.3598047"},{"key":"16_CR11","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"},{"issue":"6","key":"16_CR12","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1145\/2980983.2908099","volume":"51","author":"S Padhi","year":"2016","unstructured":"Padhi, S., Sharma, R., Millstein, T.: Data-driven precondition inference with learned features. ACM SIGPLAN Not. 51(6), 42\u201356 (2016)","journal-title":"ACM SIGPLAN Not."},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-540-77505-8_26","volume-title":"Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues","author":"C Popeea","year":"2007","unstructured":"Popeea, C., Chin, W.-N.: Inferring disjunctive postconditions. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 331\u2013345. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-77505-8_26"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Su, J., Arafat, M., Dyer, R.: Using consensus to automatically infer post-conditions. In: Proceedings of the 40th International Conference on Software Engineering: Companion Proceedings, pp. 202\u2013203 (2018)","DOI":"10.1145\/3183440.3195096"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Singleton, J.L., Leavens, G.T., Rajan, H., Cok, D.: An algorithm and tool to infer practical postconditions. In: Proceedings of the 40th International Conference on Software Engineering: Companion Proceedings, pp. 313\u2013314 (2018)","DOI":"10.1145\/3183440.3194986"},{"key":"16_CR16","unstructured":"Ryan, G., Wong, J., Yao, J., Gu, R., Jana, S.: Cln2inv: learning loop invariants with continuous logic network. In: International Conference on Learning Representations (2020)"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Yao, J., Ryan, G., Wong, J., Jana, S., Gu, R.: Learning nonlinear loop invariants with gated continuous logic networks. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 106\u2013120 (2020)","DOI":"10.1145\/3385412.3385986"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1007\/978-3-642-02658-4_48","volume-title":"Computer Aided Verification","author":"A Gupta","year":"2009","unstructured":"Gupta, A., Rybalchenko, A.: InvGen: an efficient invariant generator. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 634\u2013640. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_48"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-319-08867-9_4","volume-title":"Computer Aided Verification","author":"QL Le","year":"2014","unstructured":"Le, Q.L., Gherghina, C., Qin, S., Chin, W.-N.: Shape analysis via second-order bi-abduction. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 52\u201368. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_4"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-030-81685-8_21","volume-title":"Computer Aided Verification","author":"Q Wang","year":"2021","unstructured":"Wang, Q., Chen, M., Xue, B., Zhan, N., Katoen, J.-P.: Synthesizing invariant barrier certificates via difference-of-convex programming. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 443\u2013466. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_21"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/978-3-319-68167-2_26","volume-title":"Automated Technology for Verification and Analysis","author":"Y Feng","year":"2017","unstructured":"Feng, Y., Zhang, L., Jansen, D.N., Zhan, N., Xia, B.: Finding polynomial loop invariants for probabilistic programs. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 400\u2013416. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_26"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-53288-8_20","volume-title":"Computer Aided Verification","author":"T Gan","year":"2020","unstructured":"Gan, T., Xia, B., Xue, B., Zhan, N., Dai, L.: Nonlinear craig interpolant generation. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 415\u2013438. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_20"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Le, T.C., Qin, S., Chin, W.N.: Termination and non-termination specification inference. In: The 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 489\u2013498 (2015)","DOI":"10.1145\/2737924.2737993"},{"key":"16_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-030-53291-8_15","volume-title":"Computer Aided Verification","author":"M Vazquez-Chanlatte","year":"2020","unstructured":"Vazquez-Chanlatte, M., Seshia, S.A.: Maximum causal entropy specification inference from demonstrations. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 255\u2013278. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_15"},{"key":"16_CR25","unstructured":"OpenAI. GPT-4 technical report. CoRR arxiv:2303.08774 (2023)"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Liu, N.F., et al.: Lost in the middle: how language models use long contexts. arXiv preprint arXiv:2307.03172 (2023)","DOI":"10.1162\/tacl_a_00638"},{"key":"16_CR27","unstructured":"Baudin, P., Filli\u00e2tre, J.-C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: Acsl: Ansi\/iso c specification (2021)"},{"key":"16_CR28","unstructured":"Frama-C. Frama-c, software analyzer. Accessed 15 Jan 2024"},{"key":"16_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-46520-3_30","volume-title":"Automated Technology for Verification and Analysis","author":"S de Oliveira","year":"2016","unstructured":"de Oliveira, S., Bensalem, S., Prevosto, V.: Polynomial invariants by linear algebra. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 479\u2013494. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_30"},{"key":"16_CR30","unstructured":"Brown, T.B., et al.: Language models are few-shot learners. In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M.F., Lin, H.T. (eds.) Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, 6\u201312 December 2020, virtual (2020)"},{"key":"16_CR31","unstructured":"Frama-C. A repository dedicated for problems related to verification of programs using the tool frama-c. Accessed 15 Jan 2024"},{"key":"16_CR32","unstructured":"A rte-free x.509 parser. Accessed 15 Jan 2024"},{"key":"16_CR33","unstructured":"Alur, R., Fisman, D., Padhi, S., Singh, R., Udupa, A.: Sygus-comp 2018: results and analysis. CoRR arxiv:1904.07146 (2019)"},{"key":"16_CR34","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Li, B., McMillan, K.: Inductive invariant generation via abductive inference. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, pp. 443\u2013456. Association for Computing Machinery, New York (2013)","DOI":"10.1145\/2509136.2509511"},{"key":"16_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-030-99527-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2022","unstructured":"Beyer, D.: Progress on software verification: SV-COMP 2022. In: TACAS 2022. LNCS, vol. 13244, pp. 375\u2013402. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_20"},{"key":"16_CR36","unstructured":"Baudin, P., Bobot, F., Correnson, L., Dargaye, Z., Blanchard, A.: Wp plug-in manual. Frama-c. com (2020)"},{"key":"16_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-030-20652-9_6","volume-title":"NASA Formal Methods","author":"A Blanchard","year":"2019","unstructured":"Blanchard, A., Loulergue, F., Kosmatov, N.: Towards full proof automation in frama-C using auto-active verification. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2019. LNCS, vol. 11460, pp. 88\u2013105. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_6"},{"key":"16_CR38","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, 573\u2013609 (2015)","journal-title":"Formal Aspects Comput."},{"key":"16_CR39","doi-asserted-by":"crossref","unstructured":"Wu, Y., et al.: How effective are neural networks for fixing security vulnerabilities. In: Just, R., Fraser, G. (eds.) Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2023, Seattle, WA, USA, 17\u201321 July 2023, pp. 1282\u20131294. ACM (2023)","DOI":"10.1145\/3597926.3598135"},{"key":"16_CR40","doi-asserted-by":"publisher","unstructured":"Cosler, M., Hahn, C., Mendoza, D., Schmitt, F., Trippel, C.: nl2spec: interactively translating unstructured natural language to temporal logics with large language models. In: Enea, C., Lal, A. (eds.) Computer Aided Verification, pp. 383\u2013396. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_18","DOI":"10.1007\/978-3-031-37703-7_18"},{"key":"16_CR41","doi-asserted-by":"crossref","unstructured":"Zhai, J., et al.: C2s: translating natural language comments to formal program specifications. In: Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 25\u201337 (2020)","DOI":"10.1145\/3368089.3409716"},{"key":"16_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-030-44429-7_2","volume-title":"Requirements Engineering: Foundation for Software Quality","author":"D Giannakopoulou","year":"2020","unstructured":"Giannakopoulou, D., Pressburger, T., Mavridou, A., Schumann, J.: Generation of formal requirements from structured natural language. In: Madhavji, N., Pasquale, L., Ferrari, A., Gnesi, S. (eds.) REFSQ 2020. LNCS, vol. 12045, pp. 19\u201335. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-44429-7_2"},{"key":"16_CR43","doi-asserted-by":"crossref","unstructured":"Beckman, N.E., Nori, A.V.: Probabilistic, modular and scalable inference of typestate specifications. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 211\u2013221 (2011)","DOI":"10.1145\/1993498.1993524"},{"key":"16_CR44","doi-asserted-by":"crossref","unstructured":"Lo, D., Khoo, S.C., Liu, C.: Efficient mining of iterative patterns for software specification discovery. In: The 13th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, pp. 460\u2013469 (2007)","DOI":"10.1145\/1281192.1281243"},{"key":"16_CR45","doi-asserted-by":"crossref","unstructured":"Le, T.B.D., Lo, D.: Deep specification mining. In: Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 106\u2013117 (2018)","DOI":"10.1145\/3213846.3213876"},{"key":"16_CR46","doi-asserted-by":"crossref","unstructured":"Kang, H.J., Lo, D.: Adversarial specification mining. ACM Trans. Softw. Eng. Methodol. (TOSEM) 30(2), 1\u201340 (2021)","DOI":"10.1145\/3424307"},{"key":"16_CR47","doi-asserted-by":"crossref","unstructured":"Ammons, G., Bodik, R., Larus, J.R.: Mining specifications. ACM Sigplan Notices 37(1), 4\u201316 (2002)","DOI":"10.1145\/565816.503275"},{"key":"16_CR48","doi-asserted-by":"crossref","unstructured":"Yang, J., Evans, D., Bhardwaj, D., Bhat, T., Das, M.: Perracotta: mining temporal api rules from imperfect traces. In: Proceedings of the 28th International Conference on Software Engineering, pp. 282\u2013291 (2006)","DOI":"10.1145\/1134285.1134325"},{"key":"16_CR49","doi-asserted-by":"crossref","unstructured":"Nimmer, J.W.: Automatic generation and checking of program specifications. PhD thesis, Massachusetts Institute of Technology (2002)","DOI":"10.1145\/566172.566213"},{"issue":"6","key":"16_CR50","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/1273442.1250749","volume":"42","author":"MK Ramanathan","year":"2007","unstructured":"Ramanathan, M.K., Grama, A., Jagannathan, S.: Static specification inference using predicate mining. ACM SIGPLAN Not. 42(6), 123\u2013134 (2007)","journal-title":"ACM SIGPLAN Not."},{"key":"16_CR51","doi-asserted-by":"crossref","unstructured":"Shoham, S., Yahav, E., Fink, S., Pistoia, M.: Static specification mining using automata-based abstractions. In: Proceedings of the 2007 International Symposium on Software Testing and Analysis, pp. 174\u2013184 (2007)","DOI":"10.1145\/1273463.1273487"},{"key":"16_CR52","doi-asserted-by":"crossref","unstructured":"Lin, S.W., Sun, J., Xiao, H., Liu, Y., San\u00e1n, D., Hansen, H.: Fib: squeezing loop invariants by interpolation between forward\/backward predicate transformers. In: 2017 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 793\u2013803 (2017)","DOI":"10.1109\/ASE.2017.8115690"},{"key":"16_CR53","doi-asserted-by":"crossref","unstructured":"Molina, F., d\u2019Amorim, M., Aguirre, N.: Fuzzing class specifications. In: Proceedings of the 44th International Conference on Software Engineering, pp. 1008\u20131020 (2022)","DOI":"10.1145\/3510003.3510120"},{"key":"16_CR54","doi-asserted-by":"crossref","unstructured":"Hou, X., et al.: Large language models for software engineering: a systematic literature review. CoRR arxiv:2308.10620 (2023)","DOI":"10.1145\/3695988"},{"key":"16_CR55","doi-asserted-by":"crossref","unstructured":"Deng, Y., Xia, C.S., Peng, H., Yang, C., Zhang, L.: Large language models are zero-shot fuzzers: Fuzzing deep-learning libraries via large language models. In: Just, R., Fraser, G. (eds.) Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2023, Seattle, WA, USA, 2023, pp. 423\u2013435. ACM (2023)","DOI":"10.1145\/3597926.3598067"},{"key":"16_CR56","doi-asserted-by":"crossref","unstructured":"Lemieux, C., Inala, J.P., Lahiri, S.K., Sen, S.: Codamosa: escaping coverage plateaus in test generation with pre-trained large language models. In: 45th IEEE\/ACM International Conference on Software Engineering, ICSE 2023, Melbourne, Australia, 2023, pp. 919\u2013931. IEEE (2023)","DOI":"10.1109\/ICSE48619.2023.00085"},{"issue":"7","key":"16_CR57","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3653718","volume":"18","author":"C Wen","year":"2024","unstructured":"Wen, C., et al.: Automatically inspecting thousands of static bug warnings with large language model: how far are we? ACM Trans. Knowl. Disc. Data 18(7), 1\u201334 (2024)","journal-title":"ACM Trans. Knowl. Disc. Data"},{"key":"16_CR58","unstructured":"Sun, W., et al.: Automatic code summarization via chatgpt: how far are we? CoRR arxiv:2305.12865 (2023)"},{"key":"16_CR59","doi-asserted-by":"crossref","unstructured":"Li, H., Hao, Y., Zhai, Y., Qian, Z.: Poster: assisting static analysis with large language models: a chatgpt experiment. In: 44th IEEE Symposium on Security and Privacy, SP 2023, San Francisco, CA, USA, 2023. IEEE (2023)","DOI":"10.1145\/3611643.3613078"},{"key":"16_CR60","doi-asserted-by":"crossref","unstructured":"First, E., Rabe, M.N., Ringer, T., Brun, Y.: Baldur: whole-proof generation and repair with large language models. In: ESEC\/FSE \u201923: 31th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. ACM (2023)","DOI":"10.1145\/3611643.3616243"},{"key":"16_CR61","unstructured":"Wu, H., Barrett, C., Narodytska, N.: Lemur: integrating large language models in automated program verification. arXiv preprint arXiv:2310.04870 (2023)"},{"key":"16_CR62","unstructured":"Yang, K., et al.: Leandojo: theorem proving with retrieval-augmented language models. arXiv preprint arXiv:2306.15626 (2023)"},{"key":"16_CR63","doi-asserted-by":"crossref","unstructured":"Kang, S., Yoon, J., Yoo, S.: Large language models are few-shot testers: exploring llm-based general bug reproduction. In: 45th IEEE\/ACM International Conference on Software Engineering, ICSE 2023, Melbourne, Australia, 14\u201320 May 2023, pp. 2312\u20132323. IEEE (2023)","DOI":"10.1109\/ICSE48619.2023.00194"},{"key":"16_CR64","doi-asserted-by":"crossref","unstructured":"Pearce, H., Tan, B., Ahmad, B., Karri, R., Dolan-Gavitt, B.: Examining zero-shot vulnerability repair with large language models. In: 44th IEEE Symposium on Security and Privacy, SP 2023, San Francisco, CA, USA, 21\u201325 May 2023, pp. 2339\u20132356. IEEE (2023)","DOI":"10.1109\/SP46215.2023.10179324"},{"key":"16_CR65","doi-asserted-by":"crossref","unstructured":"Xia, C.S., Wei, Y., Zhang, L.: Automated program repair in the era of large pre-trained language models. In: 45th IEEE\/ACM International Conference on Software Engineering, ICSE 2023, Melbourne, Australia, 14\u201320 May 2023, pp. 1482\u20131494. IEEE (2023)","DOI":"10.1109\/ICSE48619.2023.00129"},{"key":"16_CR66","doi-asserted-by":"crossref","unstructured":"Fan, Z., Gao, X., Mirchev, M., Roychoudhury, A., Tan, S.H.: Automated repair of programs from large language models. In: 45th IEEE\/ACM International Conference on Software Engineering, ICSE 2023, Melbourne, Australia, 14\u201320 May 2023, pp. 1469\u20131481. IEEE (2023)","DOI":"10.1109\/ICSE48619.2023.00128"},{"key":"16_CR67","doi-asserted-by":"crossref","unstructured":"Zhai, Y., et al.: Ubitect: a precise and scalable method to detect use-before-initialization bugs in linux kernel. In: Devanbu, P., Cohen, M.B., Zimmermann, T. (eds.) ESEC\/FSE \u201920: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Virtual Event, USA, 8\u201313 November 2020, pp. 221\u2013232. ACM (2020)","DOI":"10.1145\/3368089.3409686"},{"key":"16_CR68","unstructured":"Ma, W., et al.: The scope of chatgpt in software engineering: a thorough investigation. CoRR arxiv:2305.12138 (2023)"},{"key":"16_CR69","unstructured":"Pei, K., Bieber, D., Shi, K., Sutton, C., Yin, P.: Can large language models reason about program invariants? (2023)"}],"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-65630-9_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T19:47:26Z","timestamp":1732477646000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65630-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656293","9783031656309"],"references-count":69,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65630-9_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"25 July 2024","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":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}