{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T15:47:27Z","timestamp":1759333647010,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031737404"},{"type":"electronic","value":"9783031737411"}],"license":[{"start":{"date-parts":[[2024,10,31]],"date-time":"2024-10-31T00:00:00Z","timestamp":1730332800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,10,31]],"date-time":"2024-10-31T00:00:00Z","timestamp":1730332800000},"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":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This work explores the utilization of a Large Language Model (LLM), specifically OpenAI\u2019s ChatGPT, to develop a program as a sequence of refinements. Traditionally in formal methods literature such refinements are proven correct, which can be time consuming. In this\u00a0work the refinements are tested using property-based testing. This approach addresses the problem of ensuring that the code generated by an\u00a0LLM is correct, which is one of the main challenges of code generation\u00a0with LLMs. Programs are developed in Scala and testing is performed\u00a0with ScalaCheck. This approach is demonstrated through the development and testing of a classical bridge controller, originally presented\u00a0in documentation for the refinement-based Event-B theorem prover.<\/jats:p>","DOI":"10.1007\/978-3-031-73741-1_24","type":"book-chapter","created":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T14:54:58Z","timestamp":1730300098000},"page":"385-411","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["AI-Assisted Programming with\u00a0Test-Based Refinement"],"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":[[2024,10,31]]},"reference":[{"key":"24_CR1","doi-asserted-by":"publisher","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. Theoret. Comput. Sci. 82, 253\u2013284 (1991)","journal-title":"Theoret. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)","key":"24_CR2","DOI":"10.1017\/CBO9781139195881"},{"doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Gurov, D., Johansson, M., R\u00fcmmer, P.: TriCo-triple co-piloting of implementation, specification and tests. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, ISoLA 2022, LNCS, vol. 13701, pp. 174\u2013187. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19849-6_11","key":"24_CR3","DOI":"10.1007\/978-3-031-19849-6_11"},{"issue":"2","key":"24_CR4","doi-asserted-by":"publisher","first-page":"889","DOI":"10.1007\/s10270-017-0647-0","volume":"18","author":"BK Aichernig","year":"2019","unstructured":"Aichernig, B.K., Schumi, R.: Property-based testing of web services by deriving properties from business-rule models. Softw. Syst. Model. 18(2), 889\u2013911 (2019)","journal-title":"Softw. Syst. Model."},{"doi-asserted-by":"crossref","unstructured":"Arts, T., Hughes, J., Norell, U., Svensson, H.: Testing AUTOSAR software with QuickCheck. In: Software Testing, Verification and Validation Workshops (ICSTW), 2015 IEEE Eighth International Conference on, pp. 1\u20134, April 2015","key":"24_CR5","DOI":"10.1109\/ICSTW.2015.7107466"},{"doi-asserted-by":"crossref","unstructured":"Back, R.-J., Wright, J.: Refinement Calculus - A Systematic Introduction. Texts in Computer Science (TCS) (1998)","key":"24_CR6","DOI":"10.1007\/978-1-4612-1674-2"},{"doi-asserted-by":"publisher","unstructured":"Belzner, L., Gabor, T., Wirsing, M.: Large language model assisted software engineering: prospects, challenges, and a case study. In: Steffen, B. (eds.) Bridging the Gap Between AI and Reality, AISoLA 2023, LNCS, vol. 14380, pp. 355\u2013374. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-46002-9_23","key":"24_CR7","DOI":"10.1007\/978-3-031-46002-9_23"},{"doi-asserted-by":"publisher","unstructured":"Bensalem, S., Cheng, CH., Huang, W., Huang, X., Wu, C., Zhao, X.: What, indeed, is an achievable provable guarantee for learning-enabled safety-critical systems. In: Steffen, B. (ed.) Bridging the Gap Between AI and Reality, AISoLA 2023, LNCS, vol. 14380, pp 55\u201376. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-46002-9_4","key":"24_CR8","DOI":"10.1007\/978-3-031-46002-9_4"},{"doi-asserted-by":"publisher","unstructured":"Busch, D., Nolte, G., Bainczyk, A., Steffen, B.: ChatGPT in the loop: a natural language extension for domain-specific modeling languages. In: Steffen, B. (ed.) Bridging the Gap Between AI and Reality, AISoLA 2023, LNCS, vol. 14380, pp. 375\u2013390. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-46002-9_24","key":"24_CR9","DOI":"10.1007\/978-3-031-46002-9_24"},{"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 2000, pp. 268\u2013279. New York, NY, USA, ACM (2000)","key":"24_CR10","DOI":"10.1145\/357766.351266"},{"key":"24_CR11","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, 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-030-31514-6_6","volume-title":"From Reactive Systems to Cyber-Physical Systems","author":"K Havelund","year":"2019","unstructured":"Havelund, K., Shankar, N.: A refinement proof for a garbage collector. In: Bartocci, E., Cleaveland, R., Grosu, R., Sokolsky, O. (eds.) From Reactive Systems to Cyber-Physical Systems. LNCS, vol. 11500, pp. 73\u2013103. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31514-6_6"},{"unstructured":"Jones, C.B.: Systematic Software Development Using VDM. UK, 2nd, Prentice Hall, Hemel Hempstead (1990)","key":"24_CR13"},{"issue":"3","key":"24_CR14","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"doi-asserted-by":"crossref","unstructured":"Lampropoulos, L., Sagonas, K.F.: Automatic WSDL-guided test case generation for PropEr testing of web services. In: Silva, J., Tiezzi, F. (eds.), Proceedings 8th International Workshop on Automated Specification and Verification of Web Systems, vol.\u00a098 of EPTCS, pp. 3\u201316 (2012)","key":"24_CR15","DOI":"10.4204\/EPTCS.98.3"},{"unstructured":"Morgan, C.: Programming from Specifications. Prentice Hall, Hoboken (1990)","key":"24_CR16"}],"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-031-73741-1_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T15:01:18Z","timestamp":1730300478000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-73741-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,31]]},"ISBN":["9783031737404","9783031737411"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-73741-1_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,31]]},"assertion":[{"value":"31 October 2024","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":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 October 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aisola2023","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"}}]}}