Thesis work: 30hp - Multi-function Code Generation with Automated Formal Verification

Scania

Thesis project at Traton is an excellent way of making contacts for your future working life. Many of our current employees started their career with a thesis project.

Background:

Modern truck platforms within the Traton Group rely on a growing amount of embedded software, and the demand for reliable, efficient, and maintainable code is continuously increasing. As systems grow in complexity, manually developing and maintaining software becomes time consuming and resource intensive. To address this, we investigate the use of automated code generation in an industrial automotive context. The idea is to automatically produce C code implementations from natural language descriptions or formal specifications, reducing manual coding effort while keeping consistency across software components.

For such an approach to be viable in a safety-critical setting, the generated code must be correct and compliant with internal quality standards. Instead of relying only on testing, automated verification tools can be integrated into the generation pipeline to continuously check correctness and guideline adherence. Combining automated code generation with automated verification creates a development flow that aims to produce trusted C code at higher speed while still meeting the safety and quality requirements expected in the automotive domain. This project focuses specifically on C code generation, since C is still widely used in embedded automotive systems and mature verification tools exist for this language.

Target:

The goal of this project is to explore and evaluate methods for automatically generating C software components and then verifying them automatically for correctness. The focus is on designing and testing a pipeline where code is generated for selected functions automatically, and verification tools check its correctness against functional requirements. By analyzing the outcome of this process, the project aims to refine the generation methods and assess how well this approach works and what problems occur when employing such a pipeline.

Example of assignments:

  • Create a benchmark of natural language and formal specifications for generating multi-function C code
  • Automatically infer formal specifications of subfunctions based on the main function and generate corresponding C code for the subfunctions
  • Take an existing formally verified C file and separate it into verified subfunctions
  • Evaluate differences between single-function versions and multi-function versions when automatically generating C code using LLMs.

Education:

Education: MSc in Computer Science or similar, with some background in formal methods.

Number of students: 1-2.

Start date: January/February 2026.

Estimated time needed: 20-25 weeks.

Contact person and potential supervisor:

Merlijn Sevenhuijsen, Industrial Ph.D., KTH / Traton, merlijn.sevenhuijsen@scania.com

Application:

Enclose CV, personal letter and transcript of records.

A background check might be conducted for this position.

Read Full Description
Confirmed 3 hours ago. Posted 3 days ago.

Discover Similar Jobs

Suggested Articles