Lars van den Haak
(Co-)promotors: dr.ing. Anton Wijs (TU/e), prof.dr. Marieke Huisman (UT), prof.dr. Mark van den Brand (TU/e)
Eindhoven University of Technology
Date: 19 March 2026
Thesis: PDF
Summary
This thesis addresses the problem of formally verifying optimised parallel programs.
With a survey of Stack Overflow posts, a website where many developers pose technical questions, we identified key challenges faced by GPU programmers, and we identified opportunities for formal methods researchers to investigate.
Next, we added verification support to the domain-specific language Halide with our new HaliVer tool. Halide simplifies the task of optimising, enabling exploration of multiple optimisation strategies and choose the right one for your specific parallel platform. By adding verification support at both the front-end and back-end, we allow Halide programs to be formally verified and also provide guarantees about the compilation of the generated code that Halide produces.
We applied this HaliVer approach to a case study concerning a data processing pipeline for radio telescopes. Using the optimisation power of Halide, we were able to speed up this pipeline even further. With HaliVer we tried to verify the memory safety of our algorithm. This led to new research insights and showed us the limitations of the underlying verification tools. We were able to partly solve the non-linear challenges posed by this case study. We identified that when many arrays, in our case more than 20, are present in a program, the underlying tools struggled.
In the next chapter, we show the changes we made to the VerCors deductive verification tool, which was the verifier used by HaliVer.
We introduce automatic techniques to safely rewrite nested universal quantifiers, which were crucial for the verification of the non-trivial parallel programs of the previous chapters.
To address the scalability issues, we found in the case study, we added and reused type information such that VerCors could use a better encoding when many arrays were present in the program. This encoding significantly lowers verification time and allowed for previous unverifiable programs to be verified. Both these techniques are also applicable outside the scope of HaliVer. Finally, we describe how we improved the support in VerCors for C and the GPU programming languages OpenCL and CUDA in this Chapter.
This work enables the application of formal verification to optimised parallel programs by integrating a verification approach into Halide, but also presenting techniques applicable to other parallel programming contexts. In doing so, our work provides stronger correctness guarantees for high-performance parallel applications.