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.