{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,17]],"date-time":"2026-10-17T19:17:36Z","timestamp":1792264656576,"version":"4.4.0"},"publisher-location":"Cham","reference-count":36,"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_14","type":"book-chapter","created":{"date-parts":[[2024,10,25]],"date-time":"2024-10-25T08:02:14Z","timestamp":1729843334000},"page":"222-241","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Towards AI-Assisted Correctness-by-Construction Software Development"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-9022-859X","authenticated-orcid":false,"given":"Maximilian","family":"Kodetzki","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2886-0862","authenticated-orcid":false,"given":"Tabea","family":"Bordis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9816-1504","authenticated-orcid":false,"given":"Michael","family":"Kirsten","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7153-761X","authenticated-orcid":false,"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,10,26]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice, Lecture Notes in Computer Science, vol. 10001. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Blaauwbroek, L., et al.: Learning guided automated reasoning: a brief survey. Computing Research Repository (CoRR) (2024). https:\/\/doi.org\/10.48550\/arXiv.2403.04017","DOI":"10.48550\/arXiv.2403.04017"},{"key":"14_CR3","doi-asserted-by":"publisher","unstructured":"Bordis, T., Cleophas, L., Kittelmann, A., Runge, T., Schaefer, I., Watson, B.W.: Re-CorC-Ing KeY: correct-by-construction software development based on\u00a0keY. In: The Logic of Software. A Tasting Menu of Formal Methods: Essays Dedicated to Reiner H\u00e4hnle on the Occasion of His 60th Birthday, pp. 80\u2013104. Lecture Notes in Computer Science, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-08166-8_5","DOI":"10.1007\/978-3-031-08166-8_5"},{"key":"14_CR4","doi-asserted-by":"publisher","unstructured":"Bordis, T., Runge, T., Kn\u00fcppel, A., Th\u00fcm, T., Schaefer, I.: Variational correctness-by-construction. In: VaMoS \u201920: 14th International Working Conference on Variability Modelling of Software-Intensive Systems, pp.\u00a01\u20139. ACM (2020). https:\/\/doi.org\/10.1145\/3377024.3377038","DOI":"10.1145\/3377024.3377038"},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Bounov, D., DeRossi, A., Menarini, M., Griswold, W.G., Lerner, S.: Inferring loop invariants through gamification. In: Proceedings of the 2018 CHI Conference on Human Factors in Computing Systems, pp. 1\u201413. CHI \u201918, Association for Computing Machinery, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3173574.3173805","DOI":"10.1145\/3173574.3173805"},{"key":"14_CR6","doi-asserted-by":"publisher","unstructured":"Brockschmidt, M., Chen, Y., Kohli, P., Krishna, S., Tarlow, D.: Learning shape analysis. In: Static Analysis, pp. 66\u201387. Springer International Publishing, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_4","DOI":"10.1007\/978-3-319-66706-5_4"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Chu, Z., et al.: A survey of chain of thought reasoning: advances, frontiers and future. Comput. Res. Repository (CoRR) (2023). https:\/\/doi.org\/10.48550\/arXiv.2309.15402","DOI":"10.48550\/arXiv.2309.15402"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Corso, V., Mariani, L., Micucci, D., Riganelli, O.: Generating Java Methods: An Empirical Assessment of Four AI-Based Code Assistants (2024). https:\/\/doi.org\/10.1145\/3643916.3644402","DOI":"10.1145\/3643916.3644402"},{"key":"14_CR9","doi-asserted-by":"publisher","first-page":"82434","DOI":"10.1109\/ACCESS.2022.3196347","volume":"10","author":"E Dehaerne","year":"2022","unstructured":"Dehaerne, E., Dey, B., Halder, S., De Gendt, S., Meert, W.: Code generation using machine learning: a systematic review. IEEE Access 10, 82434\u201382455 (2022). https:\/\/doi.org\/10.1109\/ACCESS.2022.3196347","journal-title":"IEEE Access"},{"issue":"8","key":"14_CR10","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975). https:\/\/doi.org\/10.1145\/360933.360975","journal-title":"Commun. ACM"},{"issue":"1","key":"14_CR11","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/BF01696781","volume":"37","author":"K G\u00f6del","year":"1930","unstructured":"G\u00f6del, K.: Die Vollst\u00e4ndigkeit Der Axiome Des Logischen Funktionenkalk\u00fcls. Monatshefte f\u00fcr Mathematik und Physik 37(1), 349\u2013360 (1930). https:\/\/doi.org\/10.1007\/BF01696781","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"key":"14_CR12","doi-asserted-by":"publisher","unstructured":"Gundersen, O.E., Kjensmo, S.: State of the art: reproducibility in artificial intelligence. In: Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, vol.\u00a032, pp. 1644\u20131651. AAAI Press (2018). https:\/\/doi.org\/10.1609\/aaai.v32i1.11503","DOI":"10.1609\/aaai.v32i1.11503"},{"key":"14_CR13","doi-asserted-by":"publisher","unstructured":"H.\u00a0Pham, L., Tran\u00a0Thi, L.L., Sun, J.: Assertion generation through active learning. In: Formal Methods and Software Engineering. Lecture Notes in Computer Science, vol. 10610, pp. 174\u2013191. Springer International Publishing, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68690-5_11","DOI":"10.1007\/978-3-319-68690-5_11"},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Jiang, A.Q., et al.: Draft, sketch, and prove: guiding formal theorem provers with informal proofs (2023). https:\/\/doi.org\/10.48550\/arXiv.2210.12283","DOI":"10.48550\/arXiv.2210.12283"},{"key":"14_CR15","doi-asserted-by":"publisher","unstructured":"Kourie, D.G., Watson, B.W.: The Correctness-by-construction Approach to Programming. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-27919-5","DOI":"10.1007\/978-3-642-27919-5"},{"key":"14_CR16","doi-asserted-by":"publisher","unstructured":"Kramer, D.: API documentation from source code comments: a case study of javadoc. In: SIGDOC99: 17th Annual International Conference on Documentation, pp. 147\u2013153. ACM (1999). https:\/\/doi.org\/10.1145\/318372.318577","DOI":"10.1145\/318372.318577"},{"key":"14_CR17","doi-asserted-by":"publisher","first-page":"111972","DOI":"10.1016\/j.jss.2024.111972","volume":"211","author":"S Lathouwers","year":"2024","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","journal-title":"J. Syst. Softw."},{"key":"14_CR18","doi-asserted-by":"publisher","unstructured":"Li, Z., et al.: A Survey on Deep Learning for Theorem Proving (2024). https:\/\/doi.org\/10.48550\/arXiv.2404.09939","DOI":"10.48550\/arXiv.2404.09939"},{"key":"14_CR19","unstructured":"Ling, Z., et al.: Deductive verification of chain-of-thought reasoning. In: Advances in Neural Information Processing Systems, vol.\u00a036, pp. 36407\u201436433. Curran Associates, Inc. (2023)"},{"key":"14_CR20","doi-asserted-by":"publisher","unstructured":"Manna, Z., Waldinger, R.: Synthesis: Dreams $$\\rightarrow $$ Programs. IEEE Trans. Softw. Eng.SE-5(4), 294\u2013328 (1979). https:\/\/doi.org\/10.1109\/TSE.1979.234198","DOI":"10.1109\/TSE.1979.234198"},{"key":"14_CR21","doi-asserted-by":"publisher","unstructured":"Mikula, M., et al.: Magnushammer: A Transformer-Based Approach to Premise Selection. CoRR arxiv preprint arxiv: abs\/2303.04488 (2023). https:\/\/doi.org\/10.48550\/arXiv.2303.04488","DOI":"10.48550\/arXiv.2303.04488"},{"key":"14_CR22","doi-asserted-by":"publisher","unstructured":"Nijkamp, E., et al.: CodeGen: An Open Large Language Model for Code with Multi-Turn Program Synthesis (2023). https:\/\/doi.org\/10.48550\/arXiv.2203.13474","DOI":"10.48550\/arXiv.2203.13474"},{"key":"14_CR23","unstructured":"OpenAI: Introducing ChatGPT. https:\/\/openai.com\/index\/chatgpt\/#OpenAI (2022)"},{"key":"14_CR24","unstructured":"Poser, N.: Evaluating AI-Assisted Software Engineering Tools. Bachelor\u2019s thesis, Karlsruhe Institute of Technology, Karlsruhe (2024)"},{"key":"14_CR25","doi-asserted-by":"publisher","unstructured":"Puri, R., et al.: CodeNet: a large-scale AI for code dataset for learning a diversity of coding tasks (2021). https:\/\/doi.org\/10.48550\/arXiv.2105.12655","DOI":"10.48550\/arXiv.2105.12655"},{"issue":"1","key":"14_CR26","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1038\/s41591-021-01614-0","volume":"28","author":"P Rajpurkar","year":"2022","unstructured":"Rajpurkar, P., Chen, E., Banerjee, O., Topol, E.J.: AI in health and medicine. Nat. Med. 28(1), 31\u201338 (2022). https:\/\/doi.org\/10.1038\/s41591-021-01614-0","journal-title":"Nat. Med."},{"key":"14_CR27","doi-asserted-by":"publisher","unstructured":"Rajpurkar Pranav, Lungren Matthew P.: The current and future state of AI interpretation of medical images. New Engl. J. Med. 388(21), 1981\u20131990 (2023). https:\/\/doi.org\/10.1056\/NEJMra2301725","DOI":"10.1056\/NEJMra2301725"},{"key":"14_CR28","doi-asserted-by":"publisher","unstructured":"Runge, T., Schaefer, I., Cleophas, L., Th\u00fcm, T., Kourie, D., Watson, B.W.: Tool support for correctness-by-construction. In: Fundamental Approaches to Software Engineering, FASE 2019. Lecture Notes in Computer Science, vol. 11424, pp. 25\u201342. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-16722-6_2","DOI":"10.1007\/978-3-030-16722-6_2"},{"key":"14_CR29","doi-asserted-by":"publisher","unstructured":"Runge, T., Th\u00fcm, T., Cleophas, L., Schaefer, I., Watson, B.W.: Comparing correctness-by-construction with post-hoc verification - a qualitative user study. In: Formal Methods. FM 2019 International Workshops. Lecture Notes in Computer Science, vol. 12233, pp. 388\u2013405. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-54997-8_25","DOI":"10.1007\/978-3-030-54997-8_25"},{"key":"14_CR30","unstructured":"Si, X., Dai, H., Raghothaman, M., Naik, M., Song, L.: Learning loop invariants for program verification. In: Advances in Neural Information Processing Systems, vol.\u00a031. Curran Associates, Inc. (2018)"},{"key":"14_CR31","unstructured":"Steinberg, D., Budinsky, F., Merks, E., Paternostro, M.: EMF: Eclipse Modeling Framework. Pearson Education (2008)"},{"issue":"2","key":"14_CR32","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/s10994-019-05855-6","volume":"109","author":"JE van Engelen","year":"2020","unstructured":"van Engelen, J.E., Hoos, H.H.: A survey on semi-supervised learning. Mach. Learn. 109(2), 373\u2013440 (2020). https:\/\/doi.org\/10.1007\/s10994-019-05855-6","journal-title":"Mach. Learn."},{"key":"14_CR33","doi-asserted-by":"publisher","unstructured":"Wang, H., et al.: LEGO-Prover: Neural Theorem Proving with Growing Libraries. CoRR arxiv preprint arxiv: abs\/2310.00656 (2023). https:\/\/doi.org\/10.48550\/arXiv.2310.00656","DOI":"10.48550\/arXiv.2310.00656"},{"key":"14_CR34","unstructured":"Wei, J., et al.: Chain-of-thought prompting elicits reasoning in large language models. In: Advances in Neural Information Processing Systems (2022)"},{"key":"14_CR35","doi-asserted-by":"publisher","unstructured":"Zhang, B., Liang, P., Zhou, X., Ahmad, A., Waseem, M.: Practices and challenges of using github copilot: an empirical study. Comput. Res. Repository (CoRR) 124\u2013129 (2023). https:\/\/doi.org\/10.18293\/SEKE2023-077","DOI":"10.18293\/SEKE2023-077"},{"key":"14_CR36","doi-asserted-by":"publisher","unstructured":"Zhao, X., Li, W., Kong, L.: Decomposing the enigma: subgoal-based demonstration learning for formal theorem proving. CoRR arxiv preprint arxiv: abs\/2305.16366 (2023). https:\/\/doi.org\/10.48550\/arXiv.2305.16366","DOI":"10.48550\/arXiv.2305.16366"}],"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_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,25]],"date-time":"2024-10-25T08:04:21Z","timestamp":1729843461000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75387-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,26]]},"ISBN":["9783031753862","9783031753879"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75387-9_14","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"}}]}}