# Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software

arXiv: https://arxiv.org/abs/2411.13269 · HTML: https://mlsanity.com/paper/2411.13269/

## 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 (most cited first, 17 of 17)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Direct Preference Optimization: Your Language Model is Secretly a Reward Model](https://mlsanity.com/paper/2305.18290/) (2023)
- [Large Language Models are Zero-Shot Reasoners](https://mlsanity.com/paper/2205.11916/) (2022)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [DSPy: Compiling Declarative Language Model Calls into Self-Improving Pipelines](https://mlsanity.com/paper/2310.03714/) (2023)
- [Language Models are Multilingual Chain-of-Thought Reasoners](https://mlsanity.com/paper/2210.03057/) (2022)
- [TextGrad: Automatic "Differentiation" via Text](https://mlsanity.com/paper/2406.07496/) (2024)
- [ChatIE: Zero-Shot Information Extraction via Chatting with ChatGPT](https://mlsanity.com/paper/2302.10205/) (2023)
- [Towards Understanding Chain-of-Thought Prompting: An Empirical Study of What Matters](https://mlsanity.com/paper/2212.10001/) (2022)
- [Is Self-Repair a Silver Bullet for Code Generation?](https://mlsanity.com/paper/2306.09896/) (2023)
- [LLMs Can't Plan, But Can Help Planning in LLM-Modulo Frameworks](https://mlsanity.com/paper/2402.01817/) (2024)
- [Bugs in Large Language Models Generated Code: An Empirical Study](https://mlsanity.com/paper/2403.08937/) (2024)
- [Teaching Temporal Logics to Neural Networks](https://mlsanity.com/paper/2003.04218/) (2020)
- [Formal Specifications from Natural Language](https://mlsanity.com/paper/2206.01962/) (2022)
- [Iterative Circuit Repair Against Formal Specifications](https://mlsanity.com/paper/2303.01158/) (2023)

## Built on by (most cited first, 2 of 2)

- [Vibe Coding vs. Agentic Coding: Fundamentals and Practical Implications of Agentic AI](https://mlsanity.com/paper/2505.19443/) (2025)
- [Survey of GenAI for Automotive Software Development: From Requirements to Executable Code](https://mlsanity.com/paper/2507.15025/) (2025)

## 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.