Research
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 2023/2024
Courses Academic Year 2022/2023
Contact Details
Visiting Address
University of Twente
Faculty of Electrical Engineering, Mathematics and Computer Science
Zilverling
(building no. 11), room 3037
Hallenweg 19
7522NH Enschede
The Netherlands
Mailing Address
University of Twente
Faculty of Electrical Engineering, Mathematics and Computer Science
Zilverling
3037
P.O. Box 217
7500 AE Enschede
The Netherlands