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.


University of Twente

Zilverling (building no. 11), room 3037
Hallenweg 19
7522 NH Enschede

Navigate to location


Scan the QR code or
Download vCard