Thesis Work 30hp - Formal Specification Inference for Automotive Software

Thesis projects at Scania are excellent ways of making contacts for your future working life. Many of our current employees started their career with a thesis project.

Background:
Modern vehicles rely heavily on software to operate properly, and Scania is among the companies aiming to sell fully autonomous vehicles within the next few years. Therefore, the correctness of software at Scania, and in the automotive industry in general, is essential. Exhaustively verifying software correctness can be done using formal verification, i.e. using mathematical reasoning to prove that a program fulfils some formal specification. However, current methods for formal verification require extensive time, resources, and knowledge, and are much geared towards greenfield projects where you use these methods from the start.

Target:
This project explores and develops methods for formal verification of software in the automotive industry. In particular, we are interested in researching how formal specifications can be constructed or refined given an existing implementation. There are several interesting use cases for such techniques, for example generating as-built documentation, filling the gap between higher-level requirements and the actual implementation for a breakdown analysis, kickstarting the use of formal verification in legacy code bases, or fine-tuning LLMs for specification and/or code generation.

Example of assignments:
•    Abductive Contract inference – Given an implementation, to what extent is abductive reasoning applicable to infer formal specifications?
•    From code to specifications using LLMs – How well are LLMs suited to generate formal specifications from an existing implementation?
•    LLM-guided specification refinement – To what extent can LLMs help increase quality of formal specifications in terms of correctness and/or completeness?

Education:
Type of project: MSc
Education: computer science, electrical engineering, engineering physics or similar, with some background in formal methods, and/or machine learning, large language models, or other AI technology.

Contact person and supervisor:
Ola Wingbrant, Research engineer, Scania, ola.wingbrant@scania.com
Mattias Nyberg, Adj. prof, KTH / Research Manager, Scania, mattias.nyberg@scania.com
Dilian Gurov, Professor, KTH, dilian@kth.se

Number of students: 1-3
Time:20 weeks, full time 40 hours per week
Start: Jan 2025
Credits: 30hp

Application:
Enclose CV, personal letter and transcript of grades.

A background check might be conducted for this position. We are conducting interviews continuously and may close the recruitment earlier than the date specified.