My research focuses on program verification, interactive theorem proving and, particularly, the challenges of making interactive proofs more automatic / scale to real code. This webpage provides a brief introduction to my research in the following areas:
- Decompilation into logic — verification of machine code
- Proof-producing synthesis from logic
- Verified Lisp and ML runtimes
- Connecting things up: verified stacks
Send me an email if you'd like to know more. My email address is at the top of the page.