{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:00:46Z","timestamp":1767999646069,"version":"3.49.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572586","type":"print"},{"value":"9783031572593","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,4,6]],"date-time":"2024-04-06T00:00:00Z","timestamp":1712361600000},"content-version":"vor","delay-in-days":96,"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>Large language models have become increasingly effective in software engineering tasks such as code generation, debugging and repair. Language models like ChatGPT can not only <jats:italic>generate<\/jats:italic> code, but also <jats:italic>explain<\/jats:italic> its inner workings and in particular its correctness. This raises the question whether we can utilize ChatGPT to support <jats:italic>formal software verification<\/jats:italic>.<\/jats:p><jats:p>In this paper, we take some first steps towards answering this question. More specifically, we investigate whether ChatGPT can generate <jats:italic>loop invariants<\/jats:italic>. Loop invariant generation is a core task in software verification, and the generation of <jats:italic>valid<\/jats:italic> and <jats:italic>useful<\/jats:italic> invariants would likely help formal verifiers. To provide some first evidence on this hypothesis, we ask ChatGPT to annotate 106 C programs with loop invariants. We check validity and usefulness of the generated invariants by passing them to two verifiers, <jats:sc>Frama-C<\/jats:sc> and CPAchecker. Our evaluation shows that ChatGPT is able to produce valid and useful invariants allowing <jats:sc>Frama-C<\/jats:sc> to verify tasks that it could not solve before. Based on our initial insights, we propose ways of combining ChatGPT (or large language models in general) and software verifiers, and discuss current limitations and open issues.<\/jats:p>","DOI":"10.1007\/978-3-031-57259-3_13","type":"book-chapter","created":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T13:01:39Z","timestamp":1712322099000},"page":"266-279","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Can ChatGPT support software verification?"],"prefix":"10.1007","author":[{"given":"Christian","family":"Jan\u00dfen","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2906-6508","authenticated-orcid":false,"given":"Cedric","family":"Richter","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2385-7512","authenticated-orcid":false,"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,6]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., H\u00e4hnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Softw. Syst. Model. 4(1), 32\u201354 (2005). https:\/\/doi.org\/10.1007\/s10270-004-0058-x, https:\/\/doi.org\/10.1007\/s10270-004-0058-x","DOI":"10.1007\/s10270-004-0058-x"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Gurov, D., Johansson, M., R\u00fcmmer, P.: Trico - triple co-piloting of implementation, specification and tests. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13701, pp. 174\u2013187. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-19849-6_11, https:\/\/doi.org\/10.1007\/978-3-031-19849-6_11","DOI":"10.1007\/978-3-031-19849-6_11"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Alon, Y., David, C.: Using graph neural networks for program termination. In: Roychoudhury, A., Cadar, C., Kim, M. (eds.) Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/FSE 2022, Singapore, Singapore, November 14-18, 2022. pp. 910\u2013921. ACM (2022). https:\/\/doi.org\/10.1145\/3540250.3549095, https:\/\/doi.org\/10.1145\/3540250.3549095","DOI":"10.1145\/3540250.3549095"},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Baudin, P., Bobot, F., B\u00fchler, D., Correnson, L., Kirchner, F., Kosmatov, N., Maroneze, A., Perrelle, V., Prevosto, V., Signoles, J., Williams, N.: The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM 64(8), 56\u201368 (2021). https:\/\/doi.org\/10.1145\/3470569, https:\/\/doi.org\/10.1145\/3470569","DOI":"10.1145\/3470569"},{"key":"13_CR5","unstructured":"Baudin, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language, http:\/\/frama-c.com\/download\/acsl.pdf"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Reliable and reproducible competition results with benchexec and witnesses (report on SV-COMP 2016). In: Chechik, M., Raskin, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016. Lecture Notes in Computer Science, vol.\u00a09636, pp. 887\u2013904. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_55, https:\/\/doi.org\/10.1007\/978-3-662-49674-9_55","DOI":"10.1007\/978-3-662-49674-9_55"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS. Lecture Notes in Computer Science, vol. 13994, pp. 495\u2013522. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29, https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: Cpachecker: A tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV. Lecture Notes in Computer Science, vol.\u00a06806, pp. 184\u2013190. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16, https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Beyer, D., Spiessl, M.: The static analyzer Frama-C in SV-COMP (competition contribution). In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022. Lecture Notes in Computer Science, vol. 13244, pp. 429\u2013434. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_26, https:\/\/doi.org\/10.1007\/978-3-030-99527-0_26","DOI":"10.1007\/978-3-030-99527-0_26"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Beyer, D., Spiessl, M., Umbricht, S.: Cooperation between automatic and interactive software verifiers. In: Schlingloff, B., Chai, M. (eds.) Software Engineering and Formal Methods - 20th International Conference, SEFM 2022. Lecture Notes in Computer Science, vol. 13550, pp. 111\u2013128. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17108-6_7, https:\/\/doi.org\/10.1007\/978-3-031-17108-6_7","DOI":"10.1007\/978-3-031-17108-6_7"},{"key":"13_CR11","unstructured":"Brown, T.B., Mann, B., Ryder, N., Subbiah, M., Kaplan, J., Dhariwal, P., Neelakantan, A., Shyam, P., Sastry, G., Askell, A., Agarwal, S., Herbert-Voss, A., Krueger, G., Henighan, T., Child, R., Ramesh, A., Ziegler, D.M., Wu, J., Winter, C., Hesse, C., Chen, M., Sigler, E., Litwin, M., Gray, S., Chess, B., Clark, J., Berner, C., McCandlish, S., Radford, A., Sutskever, I., Amodei, D.: Language models are few-shot learners. In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M., Lin, H. (eds.) Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual (2020), https:\/\/proceedings.neurips.cc\/paper\/2020\/hash\/1457c0d6bfcb4967418bfb8ac142f64a-Abstract.html"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Lahiri, S.K., Fakhoury, S., Lal, A., Musuvathi, M., Rastogi, A., Senthilnathan, A., Sharma, R., Swamy, N.: Ranking llm-generated loop invariants for program verification. In: Bouamor, H., Pino, J., Bali, K. (eds.) Findings of the Association for Computational Linguistics: EMNLP 2023, Singapore, December 6-10, 2023. pp. 9164\u20139175. Association for Computational Linguistics (2023), https:\/\/aclanthology.org\/2023.findings-emnlp.614","DOI":"10.18653\/v1\/2023.findings-emnlp.614"},{"key":"13_CR13","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Strejcek, J., Vitovsk\u00e1, M.: Joint forces for memory safety checking revisited. Int. J. Softw. Tools Technol. Transf. 22(2), 115\u2013133 (2020). https:\/\/doi.org\/10.1007\/s10009-019-00526-2, https:\/\/doi.org\/10.1007\/s10009-019-00526-2","DOI":"10.1007\/s10009-019-00526-2"},{"key":"13_CR14","unstructured":"Chen, B., Zhang, F., Nguyen, A., Zan, D., Lin, Z., Lou, J., Chen, W.: Codet: Code generation with generated tests. In: The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net (2023), https:\/\/openreview.net\/pdf?id=ktrw68Cmu9c"},{"key":"13_CR15","unstructured":"Chen, M., Tworek, J., Jun, H., Yuan, Q., de\u00a0Oliveira\u00a0Pinto, H.P., Kaplan, J., Edwards, H., Burda, Y., Joseph, N., Brockman, G., Ray, A., Puri, R., Krueger, G., Petrov, M., Khlaaf, H., Sastry, G., Mishkin, P., Chan, B., Gray, S., Ryder, N., Pavlov, M., Power, A., Kaiser, L., Bavarian, M., Winter, C., Tillet, P., Such, F.P., Cummings, D., Plappert, M., Chantzis, F., Barnes, E., Herbert-Voss, A., Guss, W.H., Nichol, A., Paino, A., Tezak, N., Tang, J., Babuschkin, I., Balaji, S., Jain, S., Saunders, W., Hesse, C., Carr, A.N., Leike, J., Achiam, J., Misra, V., Morikawa, E., Radford, A., Knight, M., Brundage, M., Murati, M., Mayer, K., Welinder, P., McGrew, B., Amodei, D., McCandlish, S., Sutskever, I., Zaremba, W.: Evaluating large language models trained on code. CoRR abs\/2107.03374 (2021), https:\/\/arxiv.org\/abs\/2107.03374"},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Chen, S., Wong, S., Chen, L., Tian, Y.: Extending context window of large language models via positional interpolation. CoRR abs\/2306.15595 (2023). https:\/\/doi.org\/10.48550\/arXiv.2306.15595, https:\/\/doi.org\/10.48550\/arXiv.2306.15595","DOI":"10.48550\/arXiv.2306.15595"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"Chen, X., Lin, M., Sch\u00e4rli, N., Zhou, D.: Teaching large language models to self-debug. CoRR abs\/2304.05128 (2023). https:\/\/doi.org\/10.48550\/arXiv.2304.05128, https:\/\/doi.org\/10.48550\/arXiv.2304.05128","DOI":"10.48550\/arXiv.2304.05128"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004. Lecture Notes in Computer Science, vol.\u00a02988, pp. 168\u2013176. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15, https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"13_CR19","doi-asserted-by":"publisher","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV: overview and verifythis competition. Int. J. Softw. Tools Technol. Transf. 17(6), 677\u2013694 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0308-3, https:\/\/doi.org\/10.1007\/s10009-014-0308-3","DOI":"10.1007\/s10009-014-0308-3"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1-3), 35\u201345 (2007). https:\/\/doi.org\/10.1016\/j.scico.2007.01.015, https:\/\/doi.org\/10.1016\/j.scico.2007.01.015","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"13_CR21","unstructured":"Fried, D., Aghajanyan, A., Lin, J., Wang, S., Wallace, E., Shi, F., Zhong, R., Yih, S., Zettlemoyer, L., Lewis, M.: Incoder: A generative model for code infilling and synthesis. In: The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net (2023), https:\/\/openreview.net\/pdf?id=hQwb-lbM6EL"},{"key":"13_CR22","doi-asserted-by":"publisher","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, January 20 - 22, 2016. pp. 499\u2013512. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837664, https:\/\/doi.org\/10.1145\/2837614.2837664","DOI":"10.1145\/2837614.2837664"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Giacobbe, M., Kroening, D., Parsert, J.: Neural termination analysis. In: Roychoudhury, A., Cadar, C., Kim, M. (eds.) Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/FSE 2022, Singapore, Singapore, November 14-18, 2022. pp. 633\u2013645. ACM (2022). https:\/\/doi.org\/10.1145\/3540250.3549120, https:\/\/doi.org\/10.1145\/3540250.3549120","DOI":"10.1145\/3540250.3549120"},{"key":"13_CR24","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a08044, pp. 36\u201352. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2, https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: Verifast: A powerful, sound, predictable, fast verifier for C and java. In: Bobaru, M.G., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06617, pp. 41\u201355. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4, https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Ji, Z., Lee, N., Frieske, R., Yu, T., Su, D., Xu, Y., Ishii, E., Bang, Y., Madotto, A., Fung, P.: Survey of hallucination in natural language generation. ACM Comput. Surv. 55(12), 248:1\u2013248:38 (2023). https:\/\/doi.org\/10.1145\/3571730, https:\/\/doi.org\/10.1145\/3571730","DOI":"10.1145\/3571730"},{"key":"13_CR27","doi-asserted-by":"publisher","unstructured":"Jiang, N., Liu, K., Lutellier, T., Tan, L.: Impact of code language models on automated program repair. In: 45th IEEE\/ACM International Conference on Software Engineering, ICSE 2023, Melbourne, Australia, May 14-20, 2023. pp. 1430\u20131442. IEEE (2023). https:\/\/doi.org\/10.1109\/ICSE48619.2023.00125, https:\/\/doi.org\/10.1109\/ICSE48619.2023.00125","DOI":"10.1109\/ICSE48619.2023.00125"},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"Kamath, A., Senthilnathan, A., Chakraborty, S., Deligiannis, P., Lahiri, S.K., Lal, A., Rastogi, A., Roy, S., Sharma, R.: Finding inductive loop invariants using large language models. CoRR abs\/2311.07948 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2311.07948, https:\/\/doi.org\/10.48550\/arXiv.2311.07948","DOI":"10.48550\/ARXIV.2311.07948"},{"key":"13_CR29","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers. Lecture Notes in Computer Science, vol.\u00a06355, pp. 348\u2013370. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20, https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"13_CR30","unstructured":"Ouyang, L., Wu, J., Jiang, X., Almeida, D., Wainwright, C.L., Mishkin, P., Zhang, C., Agarwal, S., Slama, K., Ray, A., Schulman, J., Hilton, J., Kelton, F., Miller, L., Simens, M., Askell, A., Welinder, P., Christiano, P.F., Leike, J., Lowe, R.: Training language models to follow instructions with human feedback. In: NeurIPS (2022), http:\/\/papers.nips.cc\/paper_files\/paper\/2022\/hash\/b1efde53be364a73914f58805a001731-Abstract-Conference.html"},{"key":"13_CR31","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/2908080.2908099, https:\/\/doi.org\/10.1145\/2908080.2908099","DOI":"10.1145\/2908080.2908099"},{"key":"13_CR32","unstructured":"Pei, K., Bieber, D., Shi, K., Sutton, C., Yin, P.: Can large language models reason about program invariants? In: Krause, A., Brunskill, E., Cho, K., Engelhardt, B., Sabato, S., Scarlett, J. (eds.) ICML. Proceedings of Machine Learning Research, vol.\u00a0202, pp. 27496\u201327520. PMLR (2023), https:\/\/proceedings.mlr.press\/v202\/pei23a.html"},{"key":"13_CR33","doi-asserted-by":"publisher","unstructured":"Peng, B., Galley, M., He, P., Cheng, H., Xie, Y., Hu, Y., Huang, Q., Liden, L., Yu, Z., Chen, W., Gao, J.: Check your facts and try again: Improving large language models with external knowledge and automated feedback. CoRR abs\/2302.12813 (2023). https:\/\/doi.org\/10.48550\/arXiv.2302.12813, https:\/\/doi.org\/10.48550\/arXiv.2302.12813","DOI":"10.48550\/arXiv.2302.12813"},{"key":"13_CR34","unstructured":"Rae, J.W., Borgeaud, S., Cai, T., Millican, K., Hoffmann, J., Song, H.F., Aslanides, J., Henderson, S., Ring, R., Young, S., Rutherford, E., Hennigan, T., Menick, J., Cassirer, A., Powell, R., van\u00a0den Driessche, G., Hendricks, L.A., Rauh, M., Huang, P., Glaese, A., Welbl, J., Dathathri, S., Huang, S., Uesato, J., Mellor, J., Higgins, I., Creswell, A., McAleese, N., Wu, A., Elsen, E., Jayakumar, S.M., Buchatskaya, E., Budden, D., Sutherland, E., Simonyan, K., Paganini, M., Sifre, L., Martens, L., Li, X.L., Kuncoro, A., Nematzadeh, A., Gribovskaya, E., Donato, D., Lazaridou, A., Mensch, A., Lespiau, J., Tsimpoukelli, M., Grigorev, N., Fritz, D., Sottiaux, T., Pajarskas, M., Pohlen, T., Gong, Z., Toyama, D., de\u00a0Masson\u00a0d\u2019Autume, C., Li, Y., Terzi, T., Mikulik, V., Babuschkin, I., Clark, A., de\u00a0Las\u00a0Casas, D., Guy, A., Jones, C., Bradbury, J., Johnson, M.J., Hechtman, B.A., Weidinger, L., Gabriel, I., Isaac, W., Lockhart, E., Osindero, S., Rimell, L., Dyer, C., Vinyals, O., Ayoub, K., Stanway, J., Bennett, L., Hassabis, D., Kavukcuoglu, K., Irving, G.: Scaling language models: Methods, analysis & insights from training gopher. CoRR abs\/2112.11446 (2021), https:\/\/arxiv.org\/abs\/2112.11446"},{"key":"13_CR35","unstructured":"Si, X., Dai, H., Raghothaman, M., Naik, M., Song, L.: Learning loop invariants for program verification. In: Bengio, S., Wallach, H.M., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montr\u00e9al, Canada. pp. 7762\u20137773 (2018), https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/65b1e92c585fd4c2159d5f33b5030ff2-Abstract.html"},{"key":"13_CR36","doi-asserted-by":"publisher","unstructured":"Si, X., Naik, A., Dai, H., Naik, M., Song, L.: Code2inv: A deep learning framework for program verification. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12225, pp. 151\u2013164. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_9, https:\/\/doi.org\/10.1007\/978-3-030-53291-8_9","DOI":"10.1007\/978-3-030-53291-8_9"},{"key":"13_CR37","unstructured":"Wei, J., Tay, Y., Bommasani, R., Raffel, C., Zoph, B., Borgeaud, S., Yogatama, D., Bosma, M., Zhou, D., Metzler, D., Chi, E.H., Hashimoto, T., Vinyals, O., Liang, P., Dean, J., Fedus, W.: Emergent abilities of large language models. Trans. Mach. Learn. Res. 2022 (2022), https:\/\/openreview.net\/forum?id=yzkSU5zdwD"},{"key":"13_CR38","unstructured":"Wei, J., Wang, X., Schuurmans, D., Bosma, M., Ichter, B., Xia, F., Chi, E.H., Le, Q.V., Zhou, D.: Chain-of-thought prompting elicits reasoning in large language models. In: NeurIPS (2022), http:\/\/papers.nips.cc\/paper_files\/paper\/2022\/hash\/9d5609613524ecf4f15af0f7b31abca4-Abstract-Conference.html"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57259-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T13:04:29Z","timestamp":1712322269000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57259-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572586","9783031572593"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57259-3_13","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":"6 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","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":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","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":"fase2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/fase\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"34% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}