{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T15:25:27Z","timestamp":1783610727756,"version":"3.55.0"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031754333","type":"print"},{"value":"9783031754340","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T00:00:00Z","timestamp":1735516800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T00:00:00Z","timestamp":1735516800000},"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-75434-0_9","type":"book-chapter","created":{"date-parts":[[2024,12,29]],"date-time":"2024-12-29T09:24:47Z","timestamp":1735464287000},"page":"125-144","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Towards Specification-Driven LLM-Based Generation of\u00a0Embedded Automotive Software"],"prefix":"10.1007","author":[{"given":"Minal Suresh","family":"Patil","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gustav","family":"Ung","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mattias","family":"Nyberg","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,12,30]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M.: Deductive software verification-the key book. Lect. Notes Comput. Sci. 10001 (2016)","DOI":"10.1007\/978-3-319-49812-6"},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Gurov, D., Johansson, M., R\u00fcmmer, P.: Trico-triple co-piloting of implementation, specification and tests. In: International Symposium on Leveraging Applications of Formal Methods, pp. 174\u2013187. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-19849-6_11","DOI":"10.1007\/978-3-031-19849-6_11"},{"key":"9_CR3","unstructured":"Baudin, P., Bobot, F., Correnson, L., Dargaye, Z., Blanchard, A.: WP Plug-in Manual. CEA LIST, Inria (2020). https:\/\/www.frama-c.com\/download\/frama-c-wp-manual.pdf"},{"key":"9_CR4","unstructured":"Baudin, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: Acsl: Ansi\/iso c specification (2021). https:\/\/frama-c.com\/html\/acsl.html"},{"key":"9_CR5","unstructured":"Chen, M., et\u00a0al.: Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374 (2021)"},{"key":"9_CR6","unstructured":"Conchon, S., Coquereau, A., Iguernlala, M., Mebsout, A.: Alt-ergo 2.2. In: SMT Workshop: International Workshop on Satisfiability Modulo Theories (2018)"},{"key":"9_CR7","unstructured":"Correnson, L., et al.: Frama-C User Manual. CEA LIST, Inria (2020). http:\/\/frama-c.com\/download\/frama-c-user-manual.pdf"},{"key":"9_CR8","doi-asserted-by":"publisher","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, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_18","DOI":"10.1007\/978-3-031-37703-7_18"},{"key":"9_CR9","unstructured":"Cosler, M., Schmitt, F., Hahn, C., Finkbeiner, B.: Iterative circuit repair against formal specifications. arXiv preprint arXiv:2303.01158 (2023)"},{"key":"9_CR10","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"},{"key":"9_CR11","unstructured":"Hahn, C., Schmitt, F., Kreber, J.U., Rabe, M.N., Finkbeiner, B.: Teaching temporal logics to neural networks. arXiv preprint arXiv:2003.04218 (2020)"},{"key":"9_CR12","unstructured":"Hahn, C., Schmitt, F., Tillman, J.J., Metzger, N., Siber, J., Finkbeiner, B.: Formal specifications from natural language. arXiv preprint arXiv:2206.01962 (2022)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: from pen-and-paper proofs to industrial tools. In: Computing and Software Science: State of the Art and Perspectives, pp. 345\u2013373 (2019)","DOI":"10.1007\/978-3-319-91908-9_18"},{"issue":"6","key":"9_CR14","first-page":"95","volume":"39","author":"GJ Holzmann","year":"2006","unstructured":"Holzmann, G.J.: The power of 10: rules for developing safety-critical code. Computer 39(6), 95\u201399 (2006)","journal-title":"Computer"},{"key":"9_CR15","unstructured":"International Organization for Standardization: Programming languages\u2014C. ISO\/IEC 9899:1999 (1999)"},{"key":"9_CR16","unstructured":"International Organization for Standardization: Road vehicles controller area network (CAN). ISO 11898-1:2015 (2015)"},{"key":"9_CR17","unstructured":"Kambhampati, S., et al.: Llms can\u2019t plan, but can help planning in llm-modulo frameworks. arXiv preprint arXiv:2402.01817 (2024)"},{"key":"9_CR18","unstructured":"Khattab, O., et\u00a0al.: Dspy: compiling declarative language model calls into self-improving pipelines. arXiv preprint arXiv:2310.03714 (2023)"},{"key":"9_CR19","first-page":"22199","volume":"35","author":"T Kojima","year":"2022","unstructured":"Kojima, T., Gu, S.S., Reid, M., Matsuo, Y., Iwasawa, Y.: Large language models are zero-shot reasoners. Adv. Neural. Inf. Process. Syst. 35, 22199\u201322213 (2022)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"issue":"6","key":"9_CR20","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"KRM Leino","year":"2005","unstructured":"Leino, K.R.M.: Efficient weakest preconditions. Inf. Process. Lett. 93(6), 281\u2013288 (2005)","journal-title":"Inf. Process. Lett."},{"key":"9_CR21","first-page":"3843","volume":"35","author":"A Lewkowycz","year":"2022","unstructured":"Lewkowycz, A., et al.: Solving quantitative reasoning problems with language models. Adv. Neural. Inf. Process. Syst. 35, 3843\u20133857 (2022)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Mal\u00edk, V., Vojnar, T.: Automatically checking semantic equivalence between versions of large-scale c projects. In: 2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST), pp. 329\u2013339. IEEE (2021). https:\/\/github.com\/diffkemp\/diffkemp","DOI":"10.1109\/ICST49551.2021.00045"},{"key":"9_CR23","unstructured":"MIRA Ltd: MISRA-C:2004 Guidelines for the use of the C language in critical systems (2004). https:\/\/misra.org.uk\/misra-c"},{"key":"9_CR24","unstructured":"Olausson, T.X., Inala, J.P., Wang, C., Gao, J., Solar-Lezama, A.: Demystifying gpt self-repair for code generation. arXiv preprint arXiv:2306.09896 (2023)"},{"key":"9_CR25","unstructured":"OpenAI: gpt-3.5-turbo-0125 (2022). https:\/\/www.openai.com. Accessed 25 Apr 2024"},{"key":"9_CR26","unstructured":"OpenAI: gpt-4-turbo (2023). https:\/\/www.openai.com. Accessed 25 Apr 2024"},{"key":"9_CR27","first-page":"27730","volume":"35","author":"L Ouyang","year":"2022","unstructured":"Ouyang, L., et al.: Training language models to follow instructions with human feedback. Adv. Neural. Inf. Process. Syst. 35, 27730\u201327744 (2022)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"9_CR28","unstructured":"Rafailov, R., Sharma, A., Mitchell, E., Manning, C.D., Ermon, S., Finn, C.: Direct preference optimization: your language model is secretly a reward model. Adv. Neural Inf. Process. Syst. 36 (2024)"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Ross, S.I., Martinez, F., Houde, S., Muller, M., Weisz, J.D.: The programmer\u2019s assistant: conversational interaction with a large language model for software development. In: Proceedings of the 28th International Conference on Intelligent User Interfaces, pp. 491\u2013514 (2023)","DOI":"10.1145\/3581641.3584037"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Sch\u00e4fer, M., Nadi, S., Eghbali, A., Tip, F.: An empirical evaluation of using large language models for automated unit test generation. IEEE Trans. Softw. Eng. (2023)","DOI":"10.1109\/TSE.2023.3334955"},{"key":"9_CR31","unstructured":"Shi, F., et\u00a0al.: Language models are multilingual chain-of-thought reasoners. arXiv preprint arXiv:2210.03057 (2022)"},{"key":"9_CR32","unstructured":"For Standardization\u00a0(ISO), I.O.: Iso 26262-1: 2018\u2013road vehicles-functional safety. Geneva, Switzerland (2018)"},{"key":"9_CR33","unstructured":"Tambon, F., Dakhel, A.M., Nikanjam, A., Khomh, F., Desmarais, M.C., Antoniol, G.: Bugs in large language models generated code. arXiv preprint arXiv:2403.08937 (2024)"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Ung, G., Amilon, J., Gurov, D., Lidstr\u00f6m, C., Nyberg, M., Palmskog, K.: Post-hoc formal verification of automotive software with informal requirements: an experience report. In: Accepted at 2024 IEEE 32nd International Requirements Engineering Conference (RE). IEEE (2024)","DOI":"10.1109\/RE59067.2024.00035"},{"key":"9_CR35","doi-asserted-by":"crossref","unstructured":"Vaithilingam, P., Zhang, T., Glassman, E.L.: Expectation vs. experience: evaluating the usability of code generation tools powered by large language models. In: Chi Conference on Human Factors in Computing Systems Extended Abstracts, pp.\u00a01\u20137 (2022)","DOI":"10.1145\/3491101.3519665"},{"key":"9_CR36","unstructured":"Vaswani, A., et al.: Attention is all you need. Adv. Neural Inf. Process. Syst. 30 (2017)"},{"key":"9_CR37","doi-asserted-by":"crossref","unstructured":"Wang, B., et al.: Towards understanding chain-of-thought prompting: an empirical study of what matters. arXiv preprint arXiv:2212.10001 (2022)","DOI":"10.18653\/v1\/2023.acl-long.153"},{"key":"9_CR38","unstructured":"Wei, X., et\u00a0al.: Zero-shot information extraction via chatting with chatgpt. arXiv preprint arXiv:2302.10205 (2023)"},{"key":"9_CR39","unstructured":"Wikipedia contributors: Assertion (software development)\u2014Wikipedia, the free encyclopedia (2023). https:\/\/en.wikipedia.org\/w\/index.php?title=Assertion_(software_development)&oldid=1179241560. Accessed 27 May 2024"},{"key":"9_CR40","unstructured":"Yuksekgonul, M., et al.: Textgrad: Automatic \u201cdifferentiation\" via text (2024). arXiv preprint arXiv:2406.07496"},{"key":"9_CR41","doi-asserted-by":"crossref","unstructured":"Zhong, L., Wang, Z.: Can llm replace stack overflow? a study on robustness and reliability of large language model code generation. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a038, pp. 21841\u201321849 (2024)","DOI":"10.1609\/aaai.v38i19.30185"}],"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-75434-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,29]],"date-time":"2024-12-29T10:02:52Z","timestamp":1735466572000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75434-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,30]]},"ISBN":["9783031754333","9783031754340"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75434-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,12,30]]},"assertion":[{"value":"30 December 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":"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"}}]}}