{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:45:09Z","timestamp":1768002309741,"version":"3.49.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031753862","type":"print"},{"value":"9783031753879","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,10,26]],"date-time":"2024-10-26T00:00:00Z","timestamp":1729900800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,26]],"date-time":"2024-10-26T00:00:00Z","timestamp":1729900800000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-75387-9_15","type":"book-chapter","created":{"date-parts":[[2024,10,25]],"date-time":"2024-10-25T08:02:14Z","timestamp":1729843334000},"page":"242-257","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Towards Combining the\u00a0Cognitive Abilities of\u00a0Large Language Models with\u00a0the\u00a0Rigor of\u00a0Deductive Progam Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9672-3291","authenticated-orcid":false,"given":"Bernhard","family":"Beckert","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8013-9453","authenticated-orcid":false,"given":"Jonas","family":"Klamroth","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9478-9641","authenticated-orcid":false,"given":"Wolfram","family":"Pfeifer","sequence":"additional","affiliation":[]},{"given":"Patrick","family":"R\u00f6per","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7945-9110","authenticated-orcid":false,"given":"Samuel","family":"Teuber","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,26]]},"reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-319-49812-6_15","volume-title":"Deductive Software Verification \u2013 The KeY Book","author":"W Ahrendt","year":"2016","unstructured":"Ahrendt, W., Grebing, S.: Using the KeY prover. In: Deductive Software Verification \u2013 The KeY Book. LNCS, vol. 10001, pp. 495\u2013539. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6_15"},{"key":"15_CR2","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-031-19849-6_11","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles","author":"W Ahrendt","year":"2022","unstructured":"Ahrendt, W., Gurov, D., Johansson, M., R\u00fcmmer, P.: TriCo\u2014triple co-piloting of\u00a0implementation, specification and\u00a0tests. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles. LNCS, pp. 174\u2013187. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19849-6_11"},{"key":"15_CR3","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-031-47705-8_9","volume-title":"Integrated Formal Methods","author":"L Armborst","year":"2024","unstructured":"Armborst, L., Lathouwers, S., Huisman, M.: Joining forces! Reusing contracts for\u00a0deductive verifiers through automatic Translation. In: Herber, P., Wijs, A. (eds.) Integrated Formal Methods. LNCS, pp. 153\u2013171. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-47705-8_9"},{"key":"15_CR4","doi-asserted-by":"publisher","unstructured":"Bernhard Beckert, Michael Kirsten, Jonas Klamroth, and Mattias Ulbrich. Modular verification of JML contracts using bounded model checking. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part I, volume 12476 of LNCS, pages 60\u201380. Springer, 2020. https:\/\/doi.org\/10.1007\/978-3-030-61362-4_4","DOI":"10.1007\/978-3-030-61362-4_4"},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-031-57246-3_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Beckert","year":"2024","unstructured":"Beckert, B., Sanders, P., Ulbrich, M., Wiesler, J., Witt, S.: Formally verifying an efficient sorter. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 268\u2013287. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_15"},{"key":"15_CR6","doi-asserted-by":"publisher","unstructured":"Chakraborty, S.: Ranking LLM-generated loop invariants for program verification. In Findings of the Association for Computational Linguistics: EMNLP 2023, pp. 9164\u20139175. ACL (2023). https:\/\/doi.org\/10.18653\/V1\/2023.FINDINGS-EMNLP.614","DOI":"10.18653\/V1\/2023.FINDINGS-EMNLP.614"},{"key":"15_CR7","unstructured":"Chen, M., et al.: Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374 (2021)"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-319-96145-3_10","volume-title":"Computer Aided Verification","author":"L Cordeiro","year":"2018","unstructured":"Cordeiro, L., Kesseli, P., Kroening, D., Schrammel, P., Trtik, M.: JBMC: a bounded model checking tool for verifying Java Bytecode. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification. LNCS, pp. 183\u2013190. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_10"},{"key":"15_CR9","doi-asserted-by":"publisher","unstructured":"Dakhel, A.M., Majdinasab, V., Nikanjam, A., Khomh, F., Desmarais, M.C. and Jiang, Z.M.J.: Github copilot AI pair programmer: asset or liability? J. Syst. Softw. 203, 111734 (2023). https:\/\/doi.org\/10.1016\/J.JSS.2023.111734","DOI":"10.1016\/J.JSS.2023.111734"},{"issue":"1","key":"15_CR10","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/S10817-017-9426-4","volume":"62","author":"S de Gouw","year":"2019","unstructured":"de Gouw, S., de Boer, F.S., Bubel, R., H\u00e4hnle, R., Rot, J., Steinh\u00f6fel, D.: Verifying OpenJDK\u2019s sort method for generic collections. J. Autom. Reason. 62(1), 93\u2013126 (2019). https:\/\/doi.org\/10.1007\/S10817-017-9426-4","journal-title":"J. Autom. Reason."},{"key":"15_CR11","unstructured":"Granberry, G., Ahrendt, W., Johansson, M.: Specify what? A case-study using GPT-4 and formal methods for specification synthesis. In: AI for Math Workshop at ICML 2024 (2024). https:\/\/openreview.net\/forum?id=ZRTcPkNl7v"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-030-45237-7_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H-DA Hiep","year":"2020","unstructured":"Hiep, H.-D.A., Maathuis, O., Bian, J., de Boer, F.S., van Eekelen, M., de Gouw, S.: Verifying OpenJDK\u2019s LinkedList using KeY. In: TACAS 2020. LNCS, vol. 12079, pp. 217\u2013234. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_13"},{"key":"15_CR13","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-031-57259-3_13","volume-title":"Fundamental Approaches to Software Engineering","author":"C Jan\u00dfen","year":"2024","unstructured":"Jan\u00dfen, C., Richter, C., Wehrheim, H.: Can ChatGPT support software verification? In: Beyer, D., Cavalcanti, A. (eds.) Fundamental Approaches to Software Engineering. LNCS, pp. 266\u2013279. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57259-3_13"},{"key":"15_CR14","unstructured":"Leavens, G.T., et al.: JML Reference Manual, Draft revision 2344 (2013). http:\/\/www.eecs.ucf.edu\/~leavens\/JML\/\/OldReleases\/jmlrefman.pdf"},{"key":"15_CR15","unstructured":"Kamath, A., et al.: Finding inductive loop invariants using large language models. arXiv preprint arXiv:2311.07948 (2023)"},{"key":"15_CR16","doi-asserted-by":"publisher","unstructured":"Lathouwers, S., Huisman, M.: Survey of annotation generators for deductive verifiers. J. Syst. Softw. 211, 111972 (2024). https:\/\/doi.org\/10.1016\/j.jss.2024.111972","DOI":"10.1016\/j.jss.2024.111972"},{"key":"15_CR17","unstructured":"Laurent, J., Platzer, A.: Learning to find proofs and theorems by learning to refine search strategies: the case of loop invariant synthesis. In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A. (eds.) Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022 (2022)"},{"key":"15_CR18","unstructured":"Leino, K.R.M., Moskal, M.: Usable auto-active verification. In: Ball, T., Zuck, L., Shankar, N. (eds.) Usable Verification Workshop (2010). https:\/\/fm.csl.sri.com\/UV10"},{"key":"15_CR19","unstructured":"Ni, A., et al.: NExT: teaching large language models to reason about code execution. arXiv preprint arXiv:2404.14662 (2024)"},{"key":"15_CR20","unstructured":"Pei, K., Bieber, D., Shi, K., Sutton, C., and Yin, P.: Can large language models reason about program invariants? In: Krause, A., Brunskill, E., Cho, K., Engelhardt, B., Sabato, S., Scarlett, J. (eds.) Proceedings of the 40th International Conference on Machine Learning, Proceedings of Machine Learning Research, pp. 27496\u201327520. PMLR (2023). https:\/\/proceedings.mlr.press\/v202\/pei23a.html"},{"key":"15_CR21","unstructured":"Peng, S., Kalliamvakou, E., Cihon, P., Demirer, M.: The impact of AI on developer productivity: evidence from github copilot. arXiv preprint arXiv:2302.06590 (2023)"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Intersymbolic AI: interlinking symbolic AI and subsymbolic AI. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024. LNCS, Springer, Heidelberg (2024)","DOI":"10.1007\/978-3-031-75387-9_11"},{"key":"15_CR23","unstructured":"Rozi\u00e8re, B., et al.: Code Llama: open foundation models for code. arXiv preprint arXiv:2308.12950 (2023)"},{"key":"15_CR24","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-031-65112-0_7","volume-title":"AI Verification","author":"C Sun","year":"2024","unstructured":"Sun, C., Sheng, Y., Padon, O., Barrett, C.: Clover: closed-loop verifiable code generation. In: Avni, G., et al. (eds.) AI Verification, pp. 134\u2013155. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65112-0_7"},{"key":"15_CR25","unstructured":"TouvronH., et al.: Llama: open and efficient foundation language models. arXiv preprint arXiv:2302.13971 (2023)"},{"key":"15_CR26","unstructured":"Wu, H., Barrett, C., Narodytska, N.: Lemur: integrating large language models in automated program verification. In: The Twelfth International Conference on Learning Representations (2024). https:\/\/openreview.net\/forum?id=Q3YaCghZNt"},{"key":"15_CR27","unstructured":"Yao, J., Zhou, Z., Chen, W., Cui, W.: Leveraging large language models for automated proof synthesis in rust. arXiv preprint arXiv:2311.03739 (2023)"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75387-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,30]],"date-time":"2024-11-30T07:34:18Z","timestamp":1732952058000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75387-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,26]]},"ISBN":["9783031753862","9783031753879"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75387-9_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,26]]},"assertion":[{"value":"26 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Crete","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","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":"27 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}