kth.sePublications KTH
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Generating Safety-Critical Automotive C-programs using LLMs with Formal Verification
KTH, School of Industrial Engineering and Management (ITM), Engineering Design, Mechatronics and Embedded Control Systems. Scania CV AB, Södertälje, Sweden.ORCID iD: 0009-0002-1114-4395
KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science. Scania CV AB, Södertälje, Sweden; KTH Royal Inst Technol, Stockholm, Sweden.
Scania CV AB, Södertälje, Sweden.
KTH, School of Industrial Engineering and Management (ITM). Scania CV AB, Södertälje, Sweden.ORCID iD: 0000-0001-6667-3783
2025 (English)In: Conference On Neurosymbolic Learning And Reasoning / [ed] Gilpin, LH Giunchiglia, E Hitzler, P VanKrieken, E, JMLR-JOURNAL MACHINE LEARNING RESEARCH , 2025, Vol. 284, p. 353-378Conference paper, Published paper (Refereed)
Abstract [en]

We evaluate the feasibility of generating formally verified C code that adheres to both functional and non-functional requirements using Large Language Models (LLMs) for three real industrial, automotive safety-critical software modules. We explore the capabilities of ten LLMs and four prompting techniques - Zero-Shot, Zero-Shot Chain-of-Thought, One-Shot, and One-Shot Chain-of-Thought - to generate C programs for the three modules. Functional correctness of generated programs is assessed through functional verification, and adherence to non-functional requirements is evaluated using an industrial static analyzer, along with human evaluation. The results demonstrate that it is feasible for LLMs to generate functionally correct code, with success rates of 540/800, 59/800, and 46/800 for the three modules. Additionally, the generated programs frequently adhere to the defined non-functional requirements. In the cases where the LLM-generated programs did not adhere to the non-functional requirements, deviations typically involve violations of single-read and single-write access patterns or minimal variable scope constraints. These findings highlight the promise and limitations of using LLMs to generate industrial safety-critical C programs, providing insight into improving automated LLM-based program generation in the automotive safety-critical domain.

Place, publisher, year, edition, pages
JMLR-JOURNAL MACHINE LEARNING RESEARCH , 2025. Vol. 284, p. 353-378
Series
Proceedings of Machine Learning Research, ISSN 2640-3498
National Category
Software Engineering
Identifiers
URN: urn:nbn:se:kth:diva-378979ISI: 001669525800019OAI: oai:DiVA.org:kth-378979DiVA, id: diva2:2051868
Conference
19th International Conference on Neural Symbolic Learning and Reasoning-NESY-Annual, SEP 08-10, 2025, Santa Cruz, CA
Note

QC 20260409

Available from: 2026-04-09 Created: 2026-04-09 Last updated: 2026-04-09Bibliographically approved

Open Access in DiVA

No full text in DiVA

Authority records

Sevenhuijsen, MerlijnUng, GustavNyberg, Mattias

Search in DiVA

By author/editor
Sevenhuijsen, MerlijnUng, GustavNyberg, Mattias
By organisation
Mechatronics and Embedded Control SystemsTheoretical Computer ScienceSchool of Industrial Engineering and Management (ITM)
Software Engineering

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 16 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf