My field of research is formal verification, which means applying logic to the problem of getting computer systems to work correctly.
I have written a few papers and given some talks.
I am the developer of the Metis theorem prover and one of the developers of the HOL4 theorem prover.
I helped organize the conferences TTVSI and TPHOLs 2005.
