{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T10:15:57Z","timestamp":1770977757143,"version":"3.50.1"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032104434","type":"print"},{"value":"9783032104441","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T00:00:00Z","timestamp":1762905600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T00:00:00Z","timestamp":1762905600000},"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-3-032-10444-1_16","type":"book-chapter","created":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T06:58:57Z","timestamp":1762844337000},"page":"261-278","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Specification-Guided Repair of\u00a0Arithmetic Errors in\u00a0Dafny Programs Using LLMs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-2472-8524","authenticated-orcid":false,"given":"Valentina","family":"Wu","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8060-5920","authenticated-orcid":false,"given":"Alexandra","family":"Mendes","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4198-3181","authenticated-orcid":false,"given":"Alexandre","family":"Abreu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,12]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Abreu, A., Macedo, N., Mendes, A.: Exploring automatic specification repair in dafny programs. In: 2023 38th IEEE\/ACM Int. Conference on Automated Software Engineering Workshops, ASEW, pp. 105\u2013112. IEEE ACM International Conference on Automated Software Engineering. IEEE COMPUTER SOC (2023)","DOI":"10.1109\/ASEW60602.2023.00019"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Abreu, R., Zoeteweij, P., van Gemund, A.J.: On the accuracy of spectrum-based fault localization. In: Testing: Academic and Industrial Conference Practice and Research Techniques - MUTATION, pp. 89\u201398 (2007)","DOI":"10.1109\/TAIC.PART.2007.13"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Carreira, C., Silva, \u00c1., Abreu, A., Mendes, A.: Can large language models help students prove software correctness? an experimental study with Dafny. In: 23rd Int. Conf. on Software Engineering and Formal Methods (SEFM) (2025)","DOI":"10.1007\/978-3-032-10444-1_13"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Feng, Z., et al.: CodeBERT: a pre-trained model for programming and natural languages (2020)","DOI":"10.18653\/v1\/2020.findings-emnlp.139"},{"issue":"10","key":"16_CR5","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"16_CR6","unstructured":"K\u00f6nighofer, R., Bloem, R.: Automated error localization and correction for imperative programs. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design, pp. 91\u2013100. FMCAD Inc, Austin, Texas (2011)"},{"issue":"1","key":"16_CR7","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1109\/TSE.2011.104","volume":"38","author":"C Le Goues","year":"2012","unstructured":"Le Goues, C., Nguyen, T., Forrest, S., Weimer, W.: GenProg: a generic method for automatic software repair. IEEE Trans. Software Eng. 38(1), 54\u201372 (2012)","journal-title":"IEEE Trans. Software Eng."},{"issue":"12","key":"16_CR8","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/3318162","volume":"62","author":"C Le Goues","year":"2019","unstructured":"Le Goues, C., Pradel, M., Roychoudhury, A.: Automated program repair. Commun. ACM 62(12), 56\u201365 (2019)","journal-title":"Commun. ACM"},{"issue":"4","key":"16_CR9","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1109\/MS.2021.3072577","volume":"38","author":"C Le Goues","year":"2021","unstructured":"Le Goues, C., Pradel, M., Roychoudhury, A., Chandra, S.: Automatic program repair. IEEE Softw. 38(4), 22\u201327 (2021)","journal-title":"IEEE Softw."},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Int. Conf. on Logic for Programming Artificial Intelligence and Reasoning, pp. 348\u2013370. Springer (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"16_CR11","doi-asserted-by":"publisher","first-page":"3","DOI":"10.4204\/EPTCS.149.2","volume":"149","author":"KRM Leino","year":"2014","unstructured":"Leino, K.R.M., W\u00fcstholz, V.: The dafny integrated development environment. Electron. Proc. Theor. Comput. Sci. 149, 3\u201315 (2014)","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"16_CR12","unstructured":"Loughridge, C., et al.: Dafnybench: a benchmark for formal software verification. arXiv preprint arXiv:2406.08467 (2024)"},{"key":"16_CR13","unstructured":"Meyer, B.: Design by contract. Prentice Hall Upper Saddle River (2002)"},{"key":"16_CR14","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":"16_CR15","unstructured":"Monperrus, M.: The living review on automated program repair. Technical Report hal-01956501, HAL Archives Ouvertes (2018)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"3","key":"16_CR17","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1109\/MS.2013.43","volume":"30","author":"Y Moy","year":"2013","unstructured":"Moy, Y., Ledinot, E., Delseny, H., Wiels, V., Monate, B.: Testing or formal verification: DO-178C alternatives and industrial experience. IEEE Softw. 30(3), 50\u201357 (2013)","journal-title":"IEEE Softw."},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Mugnier, E., Gonzalez, E.A., Polikarpova, N., Jhala, R., Yuanyuan, Z.: Laurel: Unblocking automated verification with large language models. Proc. ACM Program. Lang. 9(OOPSLA1) (2025)","DOI":"10.1145\/3720499"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Naveed, H., et al.: A comprehensive overview of large language models. ACM Trans. Intell. Syst. Technol. (2025)","DOI":"10.1145\/3744746"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Nguyen, H.D.T., Qi, D., Roychoudhury, A., Chandra, S.: SemFix: program repair via semantic analysis. In: 2013 35th International Conference on Software Engineering (ICSE), pp. 772\u2013781 (2013)","DOI":"10.1109\/ICSE.2013.6606623"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-030-11245-5_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T-T Nguyen","year":"2019","unstructured":"Nguyen, T.-T., Ta, Q.-T., Chin, W.-N.: Automatic Program Repair Using Formal Verification and Expression Templates. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 70\u201391. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_4"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-54804-8_17","volume-title":"Fundamental Approaches to Software Engineering","author":"Yu Pei","year":"2014","unstructured":"Pei, Yu., Furia, C.A., Nordio, M., Meyer, B.: Automatic Program Repair by Fixing Contracts. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 246\u2013260. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54804-8_17"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Pei, Y., Wei, Y., Furia, C.A., Nordio, M., Meyer, B.: Code-based automated program fixing. In: 2011 26th IEEE\/ACM International Conference on Automated Software Engineering (ASE 2011), pp. 392\u2013395 (2011)","DOI":"10.1109\/ASE.2011.6100080"},{"key":"16_CR24","unstructured":"Poesia, G., Loughridge, C., Amin, N.: dafny-annotator: AI-assisted verification of dafny programs (2024)"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Prenner, J.A., Babii, H., Robbes, R.: Can OpenAI\u2019s codex fix bugs? an evaluation on QuixBugs. In: Proc. of the Third International Workshop on Automated Program Repair, pp. 69\u201375. APR \u201922, ACM, New York (2022)","DOI":"10.1145\/3524459.3527351"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Silva, A.F., Mendes, A., Ferreira, J.F.: Leveraging large language models to boost dafny\u2019s developers productivity. In: Proceedings of the 2024 IEEE\/ACM 12th Int. Conference on Formal Methods in Software Engineering, pp. 138\u2013142. FormaliSE \u201924, Association for Computing Machinery, New York (2024)","DOI":"10.1145\/3644033.3644374"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Smith, E.K., Barr, E.T., Le\u00a0Goues, C., Brun, Y.: Is the cure worse than the disease? overfitting in automated program repair. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, pp. 532\u2013543. ESEC\/FSE 2015, Association for Computing Machinery, New York (2015)","DOI":"10.1145\/2786805.2786825"},{"key":"16_CR28","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., Giacobbe, M., Johnson, T.T., Katz, G., Lukina, A., Narodytska, N., Schilling, C. (eds.) AI Verification, pp. 134\u2013155. Springer Nature Switzerland, Cham (2024)"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"Wei, Y., Pei, Y., Furia, C.A., Silva, L.S., Buchholz, S., Meyer, B., Zeller, A.: Automated fixing of programs with contracts. In: Proceedings of the 19th International Symposium on Software testing and Analysis, pp. 61\u201372. ISSTA \u201910, Association for Computing Machinery, New York (2010)","DOI":"10.1145\/1831708.1831716"},{"issue":"1","key":"16_CR30","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1109\/TR.2013.2285319","volume":"63","author":"WE Wong","year":"2014","unstructured":"Wong, W.E., Debroy, V., Gao, R., Li, Y.: The DStar method for effective software fault localization. IEEE Trans. Reliab. 63(1), 290\u2013308 (2014)","journal-title":"IEEE Trans. Reliab."},{"issue":"8","key":"16_CR31","doi-asserted-by":"publisher","first-page":"707","DOI":"10.1109\/TSE.2016.2521368","volume":"42","author":"WE Wong","year":"2016","unstructured":"Wong, W.E., Gao, R., Li, Y., Abreu, R., Wotawa, F.: A survey on software fault localization. IEEE Trans. Softw. Eng. 42(8), 707\u2013740 (2016)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"16_CR32","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: 2023 IEEE\/ACM 45th International Conference on Software Engineering (ICSE), pp. 1482\u20131494 (2023)","DOI":"10.1109\/ICSE48619.2023.00129"},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Xia, C.S., Zhang, L.: Less training, more repairing please: revisiting automated program repair via zero-shot learning. In: Proc. of the 30th ACM Joint European Software Engineering Conf. and Symposium on the Foundations of Software Engineering, pp. 959\u2013971. ESEC\/FSE 2022, ACM, New York (2022)","DOI":"10.1145\/3540250.3549101"},{"key":"16_CR34","doi-asserted-by":"crossref","unstructured":"Zhao, H., et al.: Explainability for large language models: a survey. ACM Trans. Intell. Syst. Technol. 15(2), 20:1\u201320:38 (2024)","DOI":"10.1145\/3639372"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-10444-1_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T15:35:48Z","timestamp":1767195348000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10444-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,12]]},"ISBN":["9783032104434","9783032104441"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10444-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,12]]},"assertion":[{"value":"12 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toledo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","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":"14 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}