Flooded fens

My field of research is formal verification, which means applying mathematical logic to the problem of getting computer systems to work correctly. My Ph.D. work focused on the formal verification of probabilistic algorithms, and since then I have developed a package management system for higher order logic theories; applied automatic proof techniques for first order logic; and created the world's first formally verified chess endgame database.

I host the OpenTheory project and am the developer of the Metis theorem prover. I regularly give talks and write papers on my research, and serve on formal verification conferences.