{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T09:41:51Z","timestamp":1766050911710,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032013767"},{"type":"electronic","value":"9783032013774"}],"license":[{"start":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T00:00:00Z","timestamp":1759276800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T00:00:00Z","timestamp":1759276800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>As developers increasingly rely on Large Language Models (LLMs) to generate code, the pace of software development is accelerating beyond the capabilities of traditional design-time verification and testing methods. We predict a paradigm shift towards continuous monitoring to complement and eventually supersede upfront verification. By embracing a \u201ccorrect-ish by design\u201d philosophy, we acknowledge the inevitability of imperfections in LLM-generated code. We anticipate an adaptive approach where real-time monitoring and feedback mechanisms are employed to detect, diagnose, and rectify issues as they emerge in the field. This continuous monitoring strategy not only ensures sustained software reliability and performance, but also provides valuable insights into LLM behavior, facilitating iterative improvements. Specifically, we use an LLM to generate Python code from a formal specification written in the VDM specification language, accessible as a PDF document. The VDM specification formalizes aspects of NASA\u2019s SAFER rescue system, which uses small thrusters on a backpack to let astronauts maneuver and return safely to the spacecraft during spacewalks in case they become untethered. We experiment with property-based testing, and by using two Python programs, both generated from the specification by the LLM in two different developments, to monitor each other during runtime.<\/jats:p>","DOI":"10.1007\/978-3-032-01377-4_1","type":"book-chapter","created":{"date-parts":[[2025,9,30]],"date-time":"2025-09-30T22:24:55Z","timestamp":1759271095000},"page":"3-29","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Correct-ish by Design: From Upfront Verification to Continuous Monitoring of LLM Generated Code"],"prefix":"10.1007","author":[{"given":"Bernhard K.","family":"Aichernig","sequence":"first","affiliation":[]},{"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,10,1]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82, 253\u2013284 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge, 2010","DOI":"10.1017\/CBO9781139195881"},{"key":"1_CR3","unstructured":"Agerholm, S., Larsen, P.G.: Modeling and validating SAFER in VDM-SL. In: Lfm\u201997 - Fourth NASA Langley Formal Methods Workshop, 1997"},{"key":"1_CR4","unstructured":"Agerholm, S., Larsen, P.G.: SAFER specification in VDM-SL. Technical report, IFAD, Forskerparken 10, Odense, Denmark, 1997"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Aichernig, B.K., Havelund, K.: AI-assisted programming with test-based refinement. In: Steffen, B. (eds.) Bridging the Gap Between AI and Reality. AISoLA 2023. LNCS, vol. 14129, pp. 385\u2013411. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-73741-1_24","DOI":"10.1007\/978-3-031-73741-1_24"},{"key":"1_CR6","unstructured":"Avizienis, A.A.: The methodology of N-version programming. Softw. Fault Toler. (1995)"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-75632-5_1","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1\u201333. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_1"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08766-4","volume-title":"The Vienna Development Method: The Meta-Language","year":"1978","unstructured":"Bj\u00f8rner, D., Jones, C.B. (eds.): The Vienna Development Method: The Meta-Language. LNCS, vol. 61. Springer, Heidelberg (1978). https:\/\/doi.org\/10.1007\/3-540-08766-4"},{"key":"1_CR9","unstructured":"ChatGPT. https:\/\/chat.openai.com"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, ICFP \u201900, pp. 268\u2013279. ACM, New York, NY, USA, 2000","DOI":"10.1145\/351240.351266"},{"key":"1_CR11","unstructured":"Crow, J., et al.: Formal methods specification and analysis guidebook for the verification of software and computer systems, volume II: A practitioner\u2019s companion. Technical Report NASA-GB-O01-97, NASA, 1997"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs For Object-oriented Systems, TELOS. Springer-Verlag, Santa Clara, CA, USA (2005). https:\/\/doi.org\/10.1007\/b138800","DOI":"10.1007\/b138800"},{"key":"1_CR13","unstructured":"Fortress. https:\/\/en.wikipedia.org\/wiki\/Fortress_(programming_language)"},{"key":"1_CR14","unstructured":"Groce, A., Holzmann, G., Joshi, R., Xu, R.-G.: Putting flight software through the paces with testing, model checking, and constraint solving. In: Proceedings of the 5th International Workshop on Constraints in Formal Verification (CFV), 2008"},{"key":"1_CR15","unstructured":"Havelund, K.: Closing the gap between specification and programming: VDM$$^{++}$$ and scala. In: Korovina, M., Voronkov, A. (eds.), HOWARD-60: Higher-Order Workshop on Automated Runtime Verification and Debugging, volume\u00a01 of EasyChair Proceedings, December 2011. Manchester, UK (2011)"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Havelund, K., Reger, G.: Runtime verification logics - a language design perspective. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 310\u2013338. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63121-9_16","DOI":"10.1007\/978-3-319-63121-9_16"},{"key":"1_CR17","unstructured":"Jones, C.B.: Systematic Software Development Using VDM, second edition. Prentice Hall, Hemel Hempstead, UK (1990)"},{"key":"1_CR18","unstructured":"Larsen, P., et al.: Vienna development method specification language part 1: base language. Information Technology Programming Languages, Their Environments and System Software Interfaces, December 1996"},{"issue":"1","key":"1_CR19","first-page":"100","volume":"10","author":"W McKeeman","year":"1998","unstructured":"McKeeman, W.: Differential testing for software. Digit. Tech. J. Digit. Equip. Corp. 10(1), 100\u2013107 (1998)","journal-title":"Digit. Tech. J. Digit. Equip. Corp."},{"key":"1_CR20","unstructured":"PVS. http:\/\/pvs.csl.sri.com"}],"container-title":["Lecture Notes in Computer Science","Bridging the Gap Between AI and Reality"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-01377-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,30]],"date-time":"2025-09-30T22:24:57Z","timestamp":1759271097000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-01377-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,1]]},"ISBN":["9783032013767","9783032013774"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-01377-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,10,1]]},"assertion":[{"value":"1 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"AISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Bridging the Gap between AI and Reality","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":"30 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aisola2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/2023-aisola.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}