{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T00:50:26Z","timestamp":1772499026798,"version":"3.50.1"},"publisher-location":"Cham","reference-count":75,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031651113","type":"print"},{"value":"9783031651120","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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-65112-0_7","type":"book-chapter","created":{"date-parts":[[2024,7,16]],"date-time":"2024-07-16T20:21:48Z","timestamp":1721161308000},"page":"134-155","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["Clover: Closed-Loop Verifiable Code Generation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-9226-3688","authenticated-orcid":false,"given":"Chuyue","family":"Sun","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1883-2126","authenticated-orcid":false,"given":"Ying","family":"Sheng","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0006-4209-1635","authenticated-orcid":false,"given":"Oded","family":"Padon","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,17]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20\u201323, 2013, pp. 1\u20138. IEEE (2013). https:\/\/ieeexplore.ieee.org\/document\/6679385\/","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"7_CR2","unstructured":"Austin, J., et al.: Program synthesis with large language models. CoRR abs\/2108.07732 (2021). arXiv: 2108.07732. https:\/\/arxiv.org\/abs\/2108.07732"},{"key":"7_CR3","unstructured":"Barnes, J.: SPARK: The Proven Approach to High Integrity Software. Altran Praxis (2012)"},{"key":"7_CR4","unstructured":"Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS Press (2009)"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Bowers, M., et al.: Top-down synthesis for library learning. In: Proceedings of the ACM Program. Lang. 7(POPL), 1182\u20131213 (2023). https:\/\/doi.org\/10.1145\/3571234","DOI":"10.1145\/3571234"},{"key":"7_CR6","unstructured":"Brandfonbrener, D., et al.: Verified multi-step synthesis using large language models and monte Carlo tree search. arXiv preprint arXiv:2402.08147 (2024)"},{"key":"7_CR7","unstructured":"Bubeck, S., et al.: Sparks of artificial general intelligence: early experiments with GPT-4. arXiv preprint arXiv:2303.12712 (2023)"},{"key":"7_CR8","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves, R., van Renesse, R. (eds.) 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8\u201310, 2008, San Diego, California, USA, Proceedings, pp. 209\u2013224. USENIX Association (2008). http:\/\/www.usenix.org\/events\/osdi08\/tech\/full%5C_papers\/cadar\/cadar.pdf"},{"issue":"2","key":"7_CR9","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/2408776.2408795","volume":"56","author":"C Cadar","year":"2013","unstructured":"Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82\u201390 (2013). https:\/\/doi.org\/10.1145\/2408776.2408795","journal-title":"Commun. ACM"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Charalambous, Y., et al.: A new era in software security: towards self-healing software via large language models and formal verification. CoRR abs\/2305.14752 (2023). https:\/\/doi.org\/10.48550\/arXiv.2305.14752. arXiv: 2305.14752","DOI":"10.48550\/arXiv.2305.14752"},{"issue":"3","key":"7_CR11","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1561\/2500000049","volume":"7","author":"S Chaudhuri","year":"2021","unstructured":"Chaudhuri, S., et al.: Neurosymbolic programming. Found. Trends Program. Lang. 7(3), 158\u2013243 (2021). https:\/\/doi.org\/10.1561\/2500000049","journal-title":"Found. Trends Program. Lang."},{"key":"7_CR12","unstructured":"Chen, B., et al.: CodeT: code generation with generated tests. In: The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1\u20135, 2023. OpenReview.net (2023). https:\/\/openreview.net\/pdf?id=ktrw68Cmu9c"},{"key":"7_CR13","unstructured":"Chen, B., et al.: Codet: code generation with generated tests. arXiv preprint arXiv:2207.10397 (2022)"},{"key":"7_CR14","unstructured":"Chen, M., et al.: Evaluating large language models trained on code. CoRR abs\/2107.03374 (2021). arXiv: 2107.03374. https:\/\/arxiv.org\/abs\/2107.03374"},{"key":"7_CR15","unstructured":"Chen, X., et al.: Teaching large language models to self-debug. arXiv preprint arXiv:2304.05128 (2023)"},{"key":"7_CR16","unstructured":"Cheng, Z., et al.: Binding language models in symbolic languages. In: The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1\u20135, 2023. OpenReview.net (2023). https:\/\/openreview.net\/pdf?id=lH1PV42cbF"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Chowdhery, A., et al.: PaLM: scaling language modeling with pathways. CoRR abs\/2204.02311 (2022). https:\/\/doi.org\/10.48550\/arXiv.2204.02311. arXiv: 2204.02311. https:\/\/doi.org\/10.48550\/arXiv.2204.02311","DOI":"10.48550\/arXiv.2204.02311"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Churchill, B.R., et al.: Semantic program alignment for equivalence checking. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22\u201326, 2019, pp. 1027\u20131040. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314596","DOI":"10.1145\/3314221.3314596"},{"key":"7_CR19","unstructured":"Cobbe, K., et al.: Training verifiers to solve math word problems. CoRR abs\/2110.14168 (2021). arXiv: 2110.14168. https:\/\/arxiv.org\/abs\/2110.14168"},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"Cotroneo, D., et al.: Vulnerabilities in AI code generators: exploring targeted data poisoning attacks. CoRR abs\/2308.04451 (2023). https:\/\/doi.org\/10.48550\/arXiv.2308.04451. arXiv: 2308.04451","DOI":"10.48550\/arXiv.2308.04451"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Ding, Y., et al.: TRACED: execution-aware pre-training for source code. arXiv preprint arXiv:2306.07487 (2023)","DOI":"10.1145\/3597503.3608140"},{"key":"7_CR22","doi-asserted-by":"publisher","unstructured":"Ellis, K., et al.: DreamCoder: bootstrapping inductive program synthesis with wake-sleep library learning. In: Freund, S.N., Yahav, E. (eds.) PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20\u201325, 2021, pp. 835\u2013850. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454080","DOI":"10.1145\/3453483.3454080"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, pp. 19\u201332. American Mathematical Society (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"7_CR24","unstructured":"Ghosh, S., et al.: SpecNFS: a challenge dataset towards extracting formal models from natural language specifications. In: Calzolari, N., et al. (eds.) Proceedings of the Thirteenth Language Resources and Evaluation Conference, LREC 2022, Marseille, France, 20\u201325 June 2022, pp. 2166\u20132176. European Language Resources Association (2022). https:\/\/aclanthology.org\/2022.lrec-1.233"},{"key":"7_CR25","unstructured":"Github Copilot. Github Copilot: Your AI Pair Programmer. https:\/\/github.com\/features\/copilot"},{"issue":"1\u20132","key":"7_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1561\/2500000010","volume":"4","author":"S Gulwani","year":"2017","unstructured":"Gulwani, S., Polozov, O., Singh, R.: Program synthesis. Found. Trends Program. Lang. 4(1\u20132), 1\u2013119 (2017). https:\/\/doi.org\/10.1561\/2500000010","journal-title":"Found. Trends Program. Lang."},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"Hahn, C., et al.: Formal specifications from natural language. CoRR abs\/2206.01962 (2022). https:\/\/doi.org\/10.48550\/arXiv.2206.01962. arXiv: 2206.01962","DOI":"10.48550\/arXiv.2206.01962"},{"issue":"6632","key":"7_CR28","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1126\/science.adg4246","volume":"379","author":"J Hendler","year":"2023","unstructured":"Hendler, J.: Understanding the limits of AI coding. Science 379(6632), 548\u2013548 (2023)","journal-title":"Science"},{"key":"7_CR29","unstructured":"Hendrycks, D., et al.: Measuring coding challenge competence with APPS. In: Vanschoren, J., Yeung, S.-K. (eds.) Proceedings of the Neural Information Processing Systems Track on Datasets and Benchmarks 1, NeurIPS Datasets and Benchmarks 2021, December 2021, virtual (2021). https:\/\/datasets-benchmarks-proceedings.neurips.cc\/paper\/2021\/hash\/c24cd76e1ce41366a4bbe8a49b02a028-Abstractround2.html"},{"key":"7_CR30","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). https:\/\/doi.org\/10.1145\/363235.363259. http:\/\/doi.acm.org\/10.1145\/363235.363259","DOI":"10.1145\/363235.363259"},{"key":"7_CR31","unstructured":"Inala, J.P., et al.: Fault-aware neural code rankers. In: NeurIPS. 2022 (2022). http:\/\/papers.nips.cc\/paper%5C_files\/paper\/2022\/hash\/5762c579d09811b7639be2389b3d07be-Abstract-Conference.html"},{"key":"7_CR32","doi-asserted-by":"publisher","unstructured":"Key, D., Li, W.-D., Ellis, K.: I speak, you verify: toward trustworthy neural program synthesis. CoRR abs\/2210.00848 (2022). https:\/\/doi.org\/10.48550\/arXiv.2210.00848. arXiv: 2210.00848","DOI":"10.48550\/arXiv.2210.00848"},{"issue":"7","key":"7_CR33","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976). https:\/\/doi.org\/10.1145\/360248.360252","journal-title":"Commun. ACM"},{"key":"7_CR34","unstructured":"Lai, Y., et al.: DS-1000: a natural and reliable benchmark for data science code generation. In: Krause, A., et al. (eds.) International Conference on Machine Learning, ICML 2023, 23-29 July 2023, Honolulu, Hawaii, USA, vol. 202. Proceedings of Machine Learning Research. PMLR, 2023, pp. 18319\u201318345 (2023). https:\/\/proceedings.mlr.press\/v202\/lai23b.html"},{"key":"7_CR35","unstructured":"Lattuada, A., et al.: Verus: verifying rust programs using linear ghost types (extended version) (2023). arXiv: 2303.05491 [cs.LO]"},{"key":"7_CR36","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"7_CR37","doi-asserted-by":"publisher","unstructured":"Li, Y., et al.: On the advance of making language models better reasoners. CoRR abs\/2206.02336 (2022). https:\/\/doi.org\/10.48550\/arXiv.2206.02336. arXiv: 2206.02336","DOI":"10.48550\/arXiv.2206.02336"},{"issue":"6624","key":"7_CR38","doi-asserted-by":"publisher","first-page":"1092","DOI":"10.1126\/science.abq1158","volume":"378","author":"Y Li","year":"2022","unstructured":"Li, Y., et al.: Competition-level code generation with Alphacode. Science 378(6624), 1092\u20131097 (2022)","journal-title":"Science"},{"key":"7_CR39","unstructured":"Liu, C., et al.: Towards general loop invariant generation via coordinating symbolic execution and large language models. arXiv preprint arXiv:2311.10483 (2023)"},{"key":"7_CR40","doi-asserted-by":"publisher","unstructured":"Liu, J., et al.: Is your code generated by ChatGPT really correct? Rigorous evaluation of large language models for code generation. CoRR abs\/2305.01210 (2023). https:\/\/doi.org\/10.48550\/arXiv.2305.01210. arXiv: 2305.01210","DOI":"10.48550\/arXiv.2305.01210"},{"key":"7_CR41","unstructured":"Madaan, A., et al.: Self-refine: iterative refinement with self-feedback. In: Advances in Neural Information Processing Systems, vol. 36 (2024)"},{"issue":"2","key":"7_CR42","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/0004-3702(75)90008-9","volume":"6","author":"Z Manna","year":"1975","unstructured":"Manna, Z., Waldinger, R.: Knowledge and reasoning in program synthesis. Artif. Intell. 6(2), 175\u2013208 (1975)","journal-title":"Artif. Intell."},{"issue":"3","key":"7_CR43","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/362566.362568","volume":"14","author":"Z Manna","year":"1971","unstructured":"Manna, Z., Waldinger, R.J.: Toward automatic program synthesis. Commun. ACM 14(3), 151\u2013165 (1971)","journal-title":"Commun. ACM"},{"key":"7_CR44","doi-asserted-by":"crossref","unstructured":"Misu, Md.R.H., et al.: Towards AI-Assisted synthesis of verified Dafny methods. In: arXiv preprint arXiv:2402.00247 (2024)","DOI":"10.1145\/3643763"},{"key":"7_CR45","unstructured":"Mohammed, N., et al.: Enabling memory safety of C programs using LLMs. arXiv preprint arXiv:2404.01096 (2024)"},{"key":"7_CR46","doi-asserted-by":"crossref","unstructured":"Mondal, R., et al.: What do LLMs need to synthesize correct router configurations? In: Proceedings of the 22nd ACM Workshop on Hot Topics in Networks, pp. 189\u2013195 (2023)","DOI":"10.1145\/3626111.3628194"},{"key":"7_CR47","unstructured":"Olausson, T.X., et al.: Is self-repair a silver bullet for code generation? In: The Twelfth International Conference on Learning Representations (2023)"},{"key":"7_CR48","doi-asserted-by":"publisher","unstructured":"OpenAI. GPT-4 Technical Report. CoRR abs\/2303.08774 (2023). https:\/\/doi.org\/10.48550\/arXiv.2303.08774. arXiv: 2303.08774","DOI":"10.48550\/arXiv.2303.08774"},{"key":"7_CR49","doi-asserted-by":"crossref","unstructured":"Pan, L., et al.: Automatically correcting large language models: surveying the landscape of diverse self-correction strategies. arXiv preprint arXiv:2308.03188 (2023)","DOI":"10.1162\/tacl_a_00660"},{"key":"7_CR50","doi-asserted-by":"publisher","unstructured":"Pearce, H., et al.: Asleep at the Keyboard? Assessing the security of github copilot\u2019s code contributions. In: 43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22\u201326, 2022, pp. 754\u2013768. IEEE (2022). https:\/\/doi.org\/10.1109\/SP46214.2022.9833571","DOI":"10.1109\/SP46214.2022.9833571"},{"key":"7_CR51","unstructured":"Pei, K., et al.: Can large language models reason about program invariants? In: Krause, A., et al. (eds.) International Conference on Machine Learning, ICML 2023, 23\u201329 July 2023, Honolulu, Hawaii, USA, vol. 202. Proceedings of Machine Learning Research. PMLR, 2023, pp. 27496\u201327520 (2023). https:\/\/proceedings.mlr.press\/v202\/pei23a.html"},{"key":"7_CR52","doi-asserted-by":"publisher","unstructured":"Perry, N., et al.: Do UsersWrite more insecure code with AI assistants?\u201d CoRR abs\/2211.03622 (2022). https:\/\/doi.org\/10.48550\/arXiv.2211.03622","DOI":"10.48550\/arXiv.2211.03622"},{"key":"7_CR53","doi-asserted-by":"publisher","unstructured":"Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program synthesis from polymorphic refinement types. 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\u201317, 2016, pp. 522\u2013538. ACM (2016). https:\/\/doi.org\/10.1145\/2908080.2908093","DOI":"10.1145\/2908080.2908093"},{"key":"7_CR54","doi-asserted-by":"crossref","unstructured":"Ryan, G., et al.: Code-aware prompting: a study of coverage guided test generation in regression setting using LLM. arXiv preprint arXiv:2402.00097 (2024)","DOI":"10.1145\/3643769"},{"key":"7_CR55","unstructured":"Sandoval, G., et al.: Lost at C: a user study on the security implications of large language model code assistants. In: Joseph, A. (eds.) 32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 9\u201311, 2023. Calandrino and Carmela Troncoso. USENIX Association (2023). https:\/\/www.usenix.org\/conference\/usenixsecurity23\/presentation\/sandoval"},{"key":"7_CR56","unstructured":"Saunders. W., et al.: Self-critiquing models for assisting human evaluators. arXiv preprint arXiv:2206.05802 (2022)"},{"key":"7_CR57","doi-asserted-by":"publisher","unstructured":"Shi, F., et al.: Natural language to code translation with execution. In: Goldberg, Y., Kozareva, Z., Zhang, Y. (eds.) Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, EMNLP 2022, Abu Dhabi, United Arab Emirates, December 7\u201311, 2022, pp. 3533\u20133546. Association for Computational Linguistics (2022). https:\/\/doi.org\/10.18653\/v1\/2022.emnlp-main.231. url: https:\/\/doi.org\/10.18653\/v1\/2022.emnlp-main.231","DOI":"10.18653\/v1\/2022.emnlp-main.231"},{"key":"7_CR58","unstructured":"Shi, K., et al.: CrossBeam: learning to search in bottom-up program synthesis. In: The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25\u201329, 2022. OpenReview.net (2022). https:\/\/openreview.net\/forum?id=qhC8mr2LEKq"},{"key":"7_CR59","volume-title":"Program Synthesis by Sketching","author":"A Solar-Lezama","year":"2008","unstructured":"Solar-Lezama, A.: Program Synthesis by Sketching. University of California, Berkeley (2008)"},{"key":"7_CR60","unstructured":"Sun, C., Hahn, C., Trippel, C.: Towards improving verification productivity with circuit-aware translation of natural language to SystemVerilog assertions. In: First International Workshop on Deep Learning-aided Verification (2023)"},{"key":"7_CR61","unstructured":"Sun, C., et al.: Clover: closed-loop verifiable code generation (2024). arXiv: 2310.17807 [cs.AI]"},{"key":"7_CR62","unstructured":"Tabachnyk, M., Nikolov, S.: ML-enhanced code completion improves developer productivity. Blog (2022). https:\/\/blog.research.google\/2022\/07\/ml-enhanced-code-completion-improves.html. Accessed 26 July 2022"},{"key":"7_CR63","doi-asserted-by":"publisher","unstructured":"Udupa, A., et al.: TRANSIT: specifying protocols with concolic snippets. In: Boehm, H.-J., Flanagan, C. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201913, Seattle, WA, USA, June 16\u201319, 2013, pp. 287\u2013296. ACM (2013). https:\/\/doi.org\/10.1145\/2491956.2462174","DOI":"10.1145\/2491956.2462174"},{"key":"7_CR64","doi-asserted-by":"publisher","unstructured":"Vaithilingam, P., Zhang, T., Glassman, E.L.: Expectation vs. experience: evaluating the usability of code generation tools powered by large language models. In: Barbosa, D.J.S., et al. (eds.) CHI \u201922: CHI Conference on Human Factors in Computing Systems, New Orleans, LA, USA, 29 April 2022\u20135 May 2022, pp. 332:1\u2013332:7, Extended Abstracts. ACM (2022). https:\/\/doi.org\/10.1145\/3491101.3519665","DOI":"10.1145\/3491101.3519665"},{"key":"7_CR65","unstructured":"Waldinger, R.J., Lee, R.C.T.: PROW: a step toward automatic program writing. In: Proceedings of the 1st International Joint Conference on Artificial Intelligence, pp. 241\u2013252 (1969)"},{"key":"7_CR66","unstructured":"Wang, X., et al.: Self-consistency improves chain of thought reasoning in language models. arXiv preprint arXiv:2203.11171 (2022)"},{"key":"7_CR67","unstructured":"Wei, J., et al.: Chain-of-thought prompting elicits reasoning in large language models. In: NeurIPS (2022). http:\/\/papers.nips.cc\/paper%5C_files\/paper\/2022\/hash\/9d5609613524ecf4f15af0f7b31abca4-Abstract-Conference.html"},{"key":"7_CR68","doi-asserted-by":"crossref","unstructured":"Wen, C., et al.: Enchanting program specification synthesis by large language models using static analysis and program verification. arXiv preprint arXiv:2404.00762 (2024)","DOI":"10.1007\/978-3-031-65630-9_16"},{"key":"7_CR69","unstructured":"Wu, H., Barrett, C., Narodytska, N.: Lemur: integrating large language models in automated program verification (2023). arXiv: 2310.04870 [cs.FL]"},{"issue":"2","key":"7_CR70","doi-asserted-by":"publisher","first-page":"29:1","DOI":"10.1145\/3487569","volume":"31","author":"FF Xu","year":"2022","unstructured":"Xu, F.F., Vasilescu, B., Neubig, G.: In-IDE code generation from natural language: promise and challenges. ACM Trans. Softw. Eng. Methodol. 31(2), 29:1-29:47 (2022). https:\/\/doi.org\/10.1145\/3487569","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"7_CR71","doi-asserted-by":"publisher","unstructured":"Yin, P., Neubig, G.: A syntactic neural model for general-purpose code generation. In: Barzilay, R., Kan, M.-Y. (eds.) Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics, ACL 2017, Vancouver, Canada, July 30 - August 4, Volume 1: Long Papers, pp. 440\u2013450. Association for Computational Linguistics (2017). https:\/\/doi.org\/10.18653\/v1\/P17-1041","DOI":"10.18653\/v1\/P17-1041"},{"key":"7_CR72","doi-asserted-by":"publisher","unstructured":"Yin, P., et al.: Natural language to code generation in interactive data science notebooks. In: Rogers, A., Boyd-Graber, J.L., Okazaki, N. (eds.) Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2023, Toronto, Canada, July 9-14, 2023, pp. 126\u2013173. Association for Computational Linguistics (2023). https:\/\/doi.org\/10.18653\/v1\/2023.acl-long.9","DOI":"10.18653\/v1\/2023.acl-long.9"},{"key":"7_CR73","unstructured":"Zelikman, E., et al.: Parsel: A (de-) compositional framework for algorithmic reasoning with language models. arXiv preprint arXiv:2212.10561 (2023)"},{"key":"7_CR74","unstructured":"Zhang, T., et al.: Coder reviewer reranking for code generation. In: Krause, A., et al. (eds.) International Conference on Machine Learning, ICML 2023, 23\u201329 July 2023, Honolulu, Hawaii, USA, vol. 202. Proceedings of Machine Learning Research, pp. 41832\u201341846. PMLR (2023). https:\/\/proceedings.mlr.press\/v202\/zhang23av.html"},{"key":"7_CR75","doi-asserted-by":"publisher","unstructured":"Zhou, B., Ding, G.: Survey of intelligent program synthesis techniques. In: Saxena, S., Zhao, C. (eds.) International Conference on Algorithms, High Performance Computing, and Artificial Intelligence (AHPCAI 2023), vol. 12941. International Society for Optics and Photonics. SPIE, 2023, 129414G (2023). https:\/\/doi.org\/10.1117\/12.3011627","DOI":"10.1117\/12.3011627"}],"container-title":["Lecture Notes in Computer Science","AI Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65112-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T07:11:34Z","timestamp":1732432294000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65112-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031651113","9783031651120"],"references-count":75,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65112-0_7","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":"17 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAIV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on AI 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":"22 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"saiv2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.aiverification.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}