Focus on how software can be proven correct and secure, not just by testing, but through formal verification.
Overview
- Educational areaComputer Engineering and AI
- LanguageEnglish
Important dates
- Application opens
- Application closes
The ability to prove software correctness is especially relevant for safety-critical applications, where system failures can have severe consequences, in industries such as finance and healthcare. The specialisation covers type theory, computability, model checking, and deductive verification. It also connects to mathematics, where computer science tools are used to produce mathematically-correct proofs. Chalmers has a strong research tradition in this field, with active projects including the Agda proof assistant and the KeY system for formal verification of Java programs.
Programmes
Requirements
The requirements for the Master's programme Computer Science apply to this specialisation.
How to select a specialisation
You may choose this specialisation after you have been admitted and enrolled. Only one specialisation can be selected.