{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:23:00Z","timestamp":1762816980608,"version":"build-2065373602"},"publisher-location":"Singapore","reference-count":54,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819542123","type":"print"},{"value":"9789819542130","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T00:00:00Z","timestamp":1762819200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T00:00:00Z","timestamp":1762819200000},"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":[[2026]]},"DOI":"10.1007\/978-981-95-4213-0_6","type":"book-chapter","created":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:18:07Z","timestamp":1762816687000},"page":"97-116","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formalizing Requirements into Dafny Specifications with\u00a0LLMs"],"prefix":"10.1007","author":[{"given":"Yi-Han","family":"Lu","sequence":"first","affiliation":[]},{"given":"Xue-Yang","family":"Zhu","sequence":"additional","affiliation":[]},{"given":"Wenhui","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Rongjie","family":"Yan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,11]]},"reference":[{"key":"6_CR1","unstructured":"Achiam, J., et al.: GPT-4 technical report. arXiv preprint arXiv:2303.08774 (2023)"},{"key":"6_CR2","unstructured":"Austin, J., et al.: Program synthesis with large language models. arXiv preprint arXiv:2108.07732 (2021)"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Azaria, A., Mitchell, T.: The internal state of an LLM knows when it\u2019s lying. arXiv preprint arXiv:2304.13734 (2023)","DOI":"10.18653\/v1\/2023.findings-emnlp.68"},{"key":"6_CR4","unstructured":"Baldonado, J.M.: Semantic performance-analysis of LLM-based autoformalization. University of Buenos Aires (2024)"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Blasi, A., et al.: Translating code comments to procedure specifications. In: Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 242\u2013253 (2018)","DOI":"10.1145\/3213846.3213872"},{"key":"6_CR6","unstructured":"Cai, Y., et al.: Towards large language model aided program refinement. arXiv preprint arXiv:2406.18616 (2024)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Cassez, F., Fuller, J., Ghale, M.K., Pearce, D.J., Quiles, H.M.: Formal and executable semantics of the ethereum virtual machine in dafny. In: International Symposium on Formal Methods, pp. 571\u2013583. Springer (2023)","DOI":"10.1007\/978-3-031-27481-7_32"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., et al.: Ranking LLM-generated loop invariants for program verification. arXiv preprint arXiv:2310.09342 (2023)","DOI":"10.18653\/v1\/2023.findings-emnlp.614"},{"key":"6_CR9","doi-asserted-by":"crossref","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: International Conference on Computer Aided Verification, pp. 383\u2013396. Springer (2023)","DOI":"10.1007\/978-3-031-37703-7_18"},{"key":"6_CR10","unstructured":"Creswell, A., Shanahan, M., Higgins, I.: Selection-inference: exploiting large language models for interpretable logical reasoning. arXiv preprint arXiv:2205.09712 (2022)"},{"key":"6_CR11","unstructured":"Dafny-lang: Release_notes. https:\/\/github.com\/dafny-lang\/dafny\/blob\/master\/RELEASE_NOTES. md. Accessed 10 June 2025"},{"key":"6_CR12","unstructured":"DeepSeek: The temperature parameter. https:\/\/api-docs.deepseek.com\/quick_start\/parameter_ settings. Accessed 10 June 2025"},{"key":"6_CR13","unstructured":"Dong, Q., et al.: A survey on in-context learning. arXiv preprint arXiv:2301.00234 (2022)"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Endres, M., Fakhoury, S., Chakraborty, S., Lahiri, S.K.: Can large language models transform natural language intent into formal method postconditions? Proc. ACM Softw. Eng. 1(FSE), 1889\u20131912 (2024)","DOI":"10.1145\/3660791"},{"key":"6_CR15","unstructured":"Gao, Y., et al.: Retrieval-augmented generation for large language models: a survey. arXiv preprint arXiv:2312.109972(1) (2023)"},{"key":"6_CR16","unstructured":"Guo, D., et al.: Deepseek-r1: incentivizing reasoning capability in LLMs via reinforcement learning. arXiv preprint arXiv:2501.12948 (2025)"},{"issue":"3","key":"6_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2187671.2187678","volume":"44","author":"J Hatcliff","year":"2012","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. (CSUR) 44(3), 1\u201358 (2012)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., et al.: Ironfleet: proving practical distributed systems correct. In: Proceedings of the 25th Symposium on Operating Systems Principles, pp. 1\u201317 (2015)","DOI":"10.1145\/2815400.2815428"},{"key":"6_CR19","unstructured":"He, F., Zhai, J., Pan, M.: Beyond code generation: assessing code LLM maturity with postconditions. arXiv preprint arXiv:2407.14118 (2024)"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Irfan, A., Porncharoenwase, S., Rakamari\u0107, Z., Rungta, N., Torlak, E.: Testing dafny (experience paper). In: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 556\u2013567 (2022)","DOI":"10.1145\/3533767.3534382"},{"key":"6_CR21","unstructured":"Kamath, A., et al.: Finding inductive loop invariants using large language models. arXiv preprint arXiv:2311.07948 (2023)"},{"key":"6_CR22","unstructured":"Lahiri, S.K.: Evaluating LLM-driven user-intent formalization for verification-aware languages. arXiv preprint arXiv:2406.09757 (2024)"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp. 348\u2013370. Springer (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"6_CR24","unstructured":"Li, T., Zhang, G., Do, Q.D., Yue, X., Chen, W.: Long-context LLMs struggle with long in-context learning. arXiv preprint arXiv:2404.02060 (2024)"},{"key":"6_CR25","unstructured":"Li, Y.C., Zetzsche, S., Somayyajula, S.: Dafny as verification-aware intermediate language for code generation. arXiv preprint arXiv:2501.06283 (2025)"},{"key":"6_CR26","unstructured":"Liu, A., et al.: Deepseek-v3 technical report. arXiv preprint arXiv:2412.19437 (2024)"},{"key":"6_CR27","unstructured":"Liu, J.X., et al.: Lang2ltl: translating natural language commands to temporal specification with large language models. In: Workshop on Language and Robotics at CoRL 2022 (2022)"},{"key":"6_CR28","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":"6_CR29","doi-asserted-by":"crossref","unstructured":"Ma, L., Liu, S., Li, Y., Xie, X., Bu, L.: Specgen: automated generation of formal program specifications via large language models. arXiv preprint arXiv:2401.08807 (2024)","DOI":"10.1109\/ICSE55347.2025.00129"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"McKenna, N., Li, T., Cheng, L., Hosseini, M.J., Johnson, M., Steedman, M.: Sources of hallucination by large language models on inference tasks. arXiv preprint arXiv:2305.14552 (2023)","DOI":"10.18653\/v1\/2023.findings-emnlp.182"},{"key":"6_CR31","unstructured":"Mirchev, M., Costea, A., Singh, A.K., Roychoudhury, A.: Assured automatic programming via large language models. arXiv preprint arXiv:2410.18494 (2024)"},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"Misu, M.R.H., Lopes, C.V., Ma, I., Noble, J.: Towards AI-assisted synthesis of verified dafny methods. Proc. ACM Softw. Eng. 1(FSE), 812\u2013835 (2024)","DOI":"10.1145\/3643763"},{"key":"6_CR33","unstructured":"Mugnier, E., Anaya\u00a0Gonzalez, E., Jhala, R., Polikarpova, N., Zhou, Y.: Laurel: generating dafny assertions using large language models. arXiv e-prints pp. arXiv\u20132405 (2024)"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"Pandita, R., Xiao, X., Zhong, H., Xie, T., Oney, S., Paradkar, A.: Inferring method specifications from natural language API descriptions. In: 2012 34th International Conference on Software Engineering (ICSE), pp. 815\u2013825. IEEE (2012)","DOI":"10.1109\/ICSE.2012.6227137"},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"Pascoal\u00a0Faria, J., Trigo, E., Abreu, R.: Automatic generation of loop invariants in dafny with large language models. In: International Conference on Fundamentals of Software Engineering, pp. 138\u2013154. Springer (2025)","DOI":"10.1007\/978-3-031-87054-5_10"},{"key":"6_CR36","unstructured":"Pei, K., Bieber, D., Shi, K., Sutton, C., Yin, P.: Can large language models reason about program invariants? In: International Conference on Machine Learning, pp. 27496\u201327520. PMLR (2023)"},{"key":"6_CR37","unstructured":"Poesia, G., Loughridge, C., Amin, N.: Dafny-annotator: AI-assisted verification of dafny programs. arXiv preprint arXiv:2411.15143 (2024)"},{"key":"6_CR38","unstructured":"Sahoo, P., Singh, A.K., Saha, S., Jain, V., Mondal, S., Chadha, A.: A systematic survey of prompt engineering in large language models: Techniques and applications. arXiv preprint arXiv:2402.07927 (2024)"},{"issue":"7987","key":"6_CR39","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1038\/s41586-023-06647-8","volume":"623","author":"M Shanahan","year":"2023","unstructured":"Shanahan, M., McDonell, K., Reynolds, L.: Role play with large language models. Nature 623(7987), 493\u2013498 (2023)","journal-title":"Nature"},{"key":"6_CR40","unstructured":"Shefer, A., Engel, I., Alekseev, S., Berezun, D., Verbitskaia, E., Podkopaev, A.: Can LLMs enable verification in mainstream programming? arXiv preprint arXiv:2503.14183 (2025)"},{"key":"6_CR41","doi-asserted-by":"crossref","unstructured":"Silva, \u00c1.F., Mendes, A., Ferreira, J.F.: Leveraging large language models to boost dafny\u2019s developers productivity. In: Proceedings of the 2024 IEEE\/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE), pp. 138\u2013142 (2024)","DOI":"10.1145\/3644033.3644374"},{"key":"6_CR42","doi-asserted-by":"crossref","unstructured":"Sun, C., Sheng, Y., Padon, O., Barrett, C.: Clover: closed-loop verifiable code generation. In: International Symposium on AI Verification, pp. 134\u2013155. Springer (2024)","DOI":"10.1007\/978-3-031-65112-0_7"},{"key":"6_CR43","doi-asserted-by":"crossref","unstructured":"Tan, L., Yuan, D., Krishna, G., Zhou, Y.: \/* icomment: bugs or bad comments?*. In: Proceedings of Twenty-First ACM SIGOPS Symposium on Operating Systems Principles, pp. 145\u2013158 (2007)","DOI":"10.1145\/1294261.1294276"},{"key":"6_CR44","doi-asserted-by":"crossref","unstructured":"Tan, L., Zhou, Y., Padioleau, Y.: Acomment: mining annotations from comments and code to detect interrupt related concurrency bugs. In: Proceedings of the 33rd International Conference on Software Engineering, pp. 11\u201320 (2011)","DOI":"10.1145\/1985793.1985796"},{"key":"6_CR45","doi-asserted-by":"crossref","unstructured":"Tan, S.H., Marinov, D., Tan, L., Leavens, G.T.: @ tcomment: testing javadoc comments to detect comment-code inconsistencies. In: 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation, pp. 260\u2013269. IEEE (2012)","DOI":"10.1109\/ICST.2012.106"},{"key":"6_CR46","doi-asserted-by":"crossref","unstructured":"Wang, J., Chen, Y.: A review on code generation with LLMs: application and evaluation. In: 2023 IEEE International Conference on Medical Artificial Intelligence (MedAI), pp. 284\u2013289. IEEE (2023)","DOI":"10.1109\/MedAI59581.2023.00044"},{"issue":"3","key":"6_CR47","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3386252","volume":"53","author":"Y Wang","year":"2020","unstructured":"Wang, Y., Yao, Q., Kwok, J.T., Ni, L.M.: Generalizing from a few examples: a survey on few-shot learning. ACM Comput. Surv. (CSUR) 53(3), 1\u201334 (2020)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"6_CR48","doi-asserted-by":"crossref","unstructured":"Wang, Z.M., et al.: Rolellm: benchmarking, eliciting, and enhancing role-playing abilities of large language models. arXiv preprint arXiv:2310.00746 (2023)","DOI":"10.18653\/v1\/2024.findings-acl.878"},{"key":"6_CR49","first-page":"24824","volume":"35","author":"J Wei","year":"2022","unstructured":"Wei, J., et al.: Chain-of-thought prompting elicits reasoning in large language models. Adv. Neural. Inf. Process. Syst. 35, 24824\u201324837 (2022)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"6_CR50","doi-asserted-by":"crossref","unstructured":"Wen, C., et al.: Enchanting program specification synthesis by large language models using static analysis and program verification. In: International Conference on Computer Aided Verification, pp. 302\u2013328. Springer (2024)","DOI":"10.1007\/978-3-031-65630-9_16"},{"key":"6_CR51","doi-asserted-by":"crossref","unstructured":"Xu, Y., Feng, J., Miao, W.: Learning from failures: translation of natural language requirements into linear temporal logic with large language models. In: 2024 IEEE 24th International Conference on Software Quality, Reliability and Security (QRS), pp. 204\u2013215. IEEE (2024)","DOI":"10.1109\/QRS62785.2024.00029"},{"key":"6_CR52","unstructured":"Yu, H., et al.: Decon: detecting incorrect assertions via postconditions generated by a large language model. arXiv preprint arXiv:2501.02901 (2025)"},{"key":"6_CR53","doi-asserted-by":"crossref","unstructured":"Zhong, H., Zhang, L., Xie, T., Mei, H.: Inferring resource specifications from natural language API documentation. In: 2009 IEEE\/ACM International Conference on Automated Software Engineering, pp. 307\u2013318. IEEE (2009)","DOI":"10.1109\/ASE.2009.94"},{"key":"6_CR54","doi-asserted-by":"crossref","unstructured":"Zhou, Y., Gu, R., Chen, T., Huang, Z., Panichella, S., Gall, H.: Analyzing APIs documentation and code to detect directive defects. In: 2017 IEEE\/ACM 39th International Conference on Software Engineering (ICSE), pp. 27\u201337. IEEE (2017)","DOI":"10.1109\/ICSE.2017.11"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-4213-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:18:15Z","timestamp":1762816695000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-4213-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,11]]},"ISBN":["9789819542123","9789819542130"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-4213-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,11]]},"assertion":[{"value":"11 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hangzhou","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icfem2025.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}