Philip Tasche
(Co-)promotors: prof. dr. Marieke Huisman (UT) & prof. dr. Paula Herber (UT/University of Münster)
University of Twente
Date: 12 June 2026
Thesis: PDF
Summary
From planes to power plants, embedded systems are controlling vital functions of our society. 99% of all globally produced microcontrollers are used in embedded applications. The safety-critical nature and prevalence of these applications demand that their correctness and safety should be rigorously verified.
This thesis presents techniques to apply deductive software verification to the embedded domain and implements them in the VESUV plugin for the VerCors verifier. In two parts, it discusses advances on two problems for embedded systems verification.
The first part of this thesis discusses an invariant generation technique for verifying global properties common to embedded systems, such as timing and process interaction, locally using deductive reasoning. The invariant generation uses abstract interpretation with automatic abstraction refinement to focus in on the relevant aspects of the system under verification and abstract from unnecessary details.
The second part of this thesis describes an approach for encoding embedded software, including aspects of its execution environment, to be analyzed with a deductive verifier. It presents an approach for reasoning about concepts relevant to embedded systems, such as timing, event reactivity, and hardware interaction. It explores these concepts on the examples of two common execution environments for embedded systems, the hardware/software co-design language SystemC and the popular real-time operating system FreeRTOS, and implements encodings of both in VESUV.