My main research interest is the production of verified software by a top-down refinement process. For this, I'm using the theorem proverĀ Isabelle/HOL, for which I have developed theĀ Isabelle Refinement FrameworkĀ and theĀ Isabelle Collection Framework.Ā It has been used to verify model checkers, and the GRAT unsat verificationĀ tool.
I'm developing the Isabelle-LLVM tool, which can be used to refine algorithms down to efficient imperative code. Highlights are efficient verified (parallel) sorting algorithms, and the verified IsaSAT -Solver.
For a complete list of publications, see DBLP.
Courses academic year 2025/2026
Courses in the current academic year are added at the moment they are finalised in the Osiris system. Therefore it is possible that the list is not yet complete for the whole academic year.
Courses academic year 2024/2025
Address
University of Twente
Zilverling (building no. 11), room 3037
Hallenweg 19
7522 NH Enschede
Netherlands
University of Twente
Zilverling 3037
P.O. Box 217
7500 AE Enschede
Netherlands
Scan the QR code or