notesum.ai
Published at November 20Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software
cs.SE
cs.AI
Released Date: November 20, 2024
Authors: Minal Suresh Patil1, Gustav Ung2, Mattias Nyberg2
Aff.: 1Umeå Universitet, 90187 Umeå, Sweden; 2Scania, Granparksvägen 10, 15148 Södertälje, Sweden
| Model | Specification Type | Compile | Eq. Check | Verified (Proved Goals) | LoC |
|---|---|---|---|---|---|
| GPT-4-turbo | ACSL | Yes | Not Eq | 41 / 50 | 48 |
| HLNL | Yes | Not Eq | 13 / 26 | 21 | |
| LLNL | Yes | Not Eq | 39 / 40 | 48 | |
| ACSL + HLNL + LLNL | Yes | Not Eq | 40 / 52 | 64 | |
| HLNL + LLNL | Yes | Not Eq | 30 / 30 | 32 | |
| ACSL + LLNL | Yes | Not Eq | 39 / 40 | 65 | |
| ACSL + HLNL | Yes | Not Eq | 41 / 52 | 30 | |
| GPT-3.5 | ACSL | Yes | Not Eq | 41 / 43 | 36 |
| HLNL | Yes | Not Eq | 11 / 24 | 20 | |
| LLNL | No | n/a | n/a | n/a | |
| ACSL + HLNL + LLNL | Yes | Not Eq | 39 / 40 | 44 | |
| HLNL + LLNL | No | n/a | n/a | n/a | |
| ACSL + LLNL | Yes | Not Eq | 13 / 30 | 35 | |
| ACSL + HLNL | Yes | Not Eq | 38 / 42 | 33 |