Cookies
The University of Twente websites use cookies to analyse website usage and improve usability. We also use third party tracking-cookies to measure user preferences, enable content sharing on social media and interest-based advertising.
Cookie policy

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.

Scan the QR code or
Download vCard