Master's Thesis: Probabilistic Formal Verification
Confirmed on the employer's own hiring board on Nov 1, 2026. First seen by Alion on Oct 30, 2026. Scania scores A on the Alion truth index.
30hp Formal Verification of Probabilistic Automotive Systems
Introduction:
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 increasingly on computers 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 systemcorrectness can be done using formal verification, which means using mathematical reasoning to prove that a systemfulfilssome formal specification. However, current methods for formal verification require extensive time, resources and knowledge, and have therefore not yet been widely adopted in the automotive industry.
When driving inthe real world, probabilities often arise due to random hardware failures, stochastic communication delays, sensor ghost objects, machine learning components, rounding errors, human behavior, and probabilistic algorithms.
Therefore, vehicle specifications must take probabilities into account. Using probabilistic contracts to specify allowed vehicle behaviors, checking that a vehicle fulfils its contract can be done according to the following three steps:
Decompose the vehicle contract into component contracts.
Verify the correctness of the decomposition.
Verify that each component fulfils its contract.
In most cases, current techniques for formal verification lack the generality and efficiency to successfully complete the above three steps.
Objective:
The goal of this project is to investigatehowprobabilistic reasoningcan be used to checkifan autonomous vehicle fulfils its specifications. For instance, given a black-box model M of an autonomous vehicle and a specification S stating that “reindeer on the road are correctly identified 99.9% of the time, with each correct identification resulting in a 95% probability of avoidance”, is it possible to determine whether M fulfils S?
Since rounding errors of floats can be viewed as probabilistic, it may also be possible to verify code against specifications using statistical methods.
Examples of assignment:
Probabilistic modeling of vehicles or components
Formulating probabilistic specifications for vehicles or components
Model checking against probabilistic specifications using hypothesis testing
Specifying rounding errors in software using probabilities
Verifying C code against formal specifications using hypothesis testing
Investigatinghypothesis testing for nested probabilities
Monte Carlo simulation for the verification of probabilistic specifications
We are also interested in hearing other ideas for directions of the thesis, which can bediscussed before the start to better match the applicant’s interest and background.
Education/program/focus:
M.Sc. in Engineering or similar with an interest incomputer science, probability theory, or formal methods.
Number of students: 1-3.
Start date: January 2026.
Estimated time needed: 20 weeks.
Contact person and supervisor:
Anton Hampus, PhD student, +46737787449,[email protected]
Application:
Your application must include a 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.
Publication date:
2026-10-22- 2026-11-10