Thesis Work 30hp - Formal Verification Techniques for Software Reliability of Automotive Software

A thesis project at Scania 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 vehicles rely heavily on software to operate properly. In order to keep traffic participants safe, the correct functioning of these vehicles must be ensured. Therefore, the correctness of software at Scania, and in the automotive industry in general, is essential. Currently, correctness is often shown using non-exhaustive methods, such as software testing. A different, exhaustive approach is to verify software correctness using formal verification, which means using mathematical reasoning to prove that a program fulfils a formal specification. As the complexity of the software grows in newer vehicles, there is a demand for means of dealing with this complexity, such as turning to more sophisticated programming languages. Therefore, there is a need to extend formal verification to future industrially relevant programming languages.

Target:
In general, formal verification gives a higher level of trust in the software than, for example, software testing. This project explores and develops methods for formal verification of software in the automotive industry. In particular, we are interested in researching how current methods and tools for formal verification can be made more accessible for future industrial systems. Areas of interest include deductive verification performed directly on C++/Rust code, as well as formal verification of software based on the AUTOSAR framework. Other related topics we are interested in include automatic program instrumentation techniques to enhance the verification process and the use of LLMs for generating verifiable code.

Example of assignments:
•    Verification of C++ Code Using State-of-the-Art Tools: Compare various state-of-the-art tools for verifying C++ code based on criteria such as: feature support in the language, contract language support, scalability, and modularity. 
•    Verification of Rust Code Using State-of-the-Art Tools: Compare different state-of-the-art tools for verifying code based on criteria such as: feature support in the language, contract language support, scalability, and modularity.
•    Rust, C++, or Dafny code generation using LLMs combined with formal verification. This focuses on employing techniques to generate code, which then is formally verified to ensure it is correct.
•    Case study on formal verification of software based on AUTOSAR Adaptive (or Classic) for C++. This explores the methodologies and tools used to ensure the correctness and reliability of automotive software within the AUTOSAR framework.
•    Automatic program instrumentation techniques for enhancing deductive verification of embedded systems software. This examines how automatic instrumentation can streamline the deductive verification of software, thus improving efficiency in the verification workflow for embedded systems. 
•    We are also interested in hearing and discussing other ideas for directions of the thesis.

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

Contact persons:
Merlijn Sevenhuijsen, Industrial Ph.D., KTH & Scania, merlijn.sevenhuijsen@scania.com
Mattias Nyberg, Adj. prof, KTH / Research Lead, Scania,  mattias.nyberg@scania.com

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.