Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software
Not on the map. Why?
Abstract (arXiv)
The paper studies how code generation by LLMs can be combined with formal verification to produce critical embedded software. The first contribution is a general framework, spec2code, in which LLMs are combined with different types of critics that produce feedback for iterative backprompting and fine-tuning. The second contribution presents a first feasibility study, where a minimalistic instantiation of spec2code, without iterative backprompting and fine-tuning, is empirically evaluated using three industrial case studies from the heavy vehicle manufacturer Scania. The goal is to automatically generate industrial-quality code from specifications only. Different combinations of formal ACSL specifications and natural language specifications are explored. The results indicate that formally correct code can be generated even without the application of iterative backprompting and fine-tuning.
Key facts. Cited by 2 papers in the map (data through 14 Oct 2026). Builds on 17 of its 41 references that are in the map. First posted on arXiv 20 Nov 2024.
Builds on
17 of 41 references.
References · 17
- 2017Attention Is All You Needcited by 60,361
- 2022Training language models to follow instructions with human feedbackcited by 15,971
- 2021Evaluating Large Language Models Trained on Codecited by 8,320
- 2023Direct Preference Optimization: Your Language Model is Secretly a Reward Modelcited by 8,065
- 2022Large Language Models are Zero-Shot Reasonerscited by 4,374
- 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,392
- 2023DSPy: Compiling Declarative Language Model Calls into Self-Improving Pipelinescited by 832
- 2022Language Models are Multilingual Chain-of-Thought Reasonerscited by 530
- 2024TextGrad: Automatic "Differentiation" via Textcited by 273
- 2023ChatIE: Zero-Shot Information Extraction via Chatting with ChatGPTcited by 250
- 2022Towards Understanding Chain-of-Thought Prompting: An Empirical Study of What Matterscited by 222
- 2023Is Self-Repair a Silver Bullet for Code Generation?cited by 197
5 more
- 2024LLMs Can't Plan, But Can Help Planning in LLM-Modulo Frameworkscited by 179
- 2024Bugs in Large Language Models Generated Code: An Empirical Studycited by 60
- 2020Teaching Temporal Logics to Neural Networkscited by 51
- 2022Formal Specifications from Natural Languagecited by 33
- 2023Iterative Circuit Repair Against Formal Specificationscited by 9
Built on by
Citing papers per year: 2025: 2.
2 papers.