I finished my Ph.D in 2011 in the Computer Science department at Stanford. My research focused on formal verification, and my advisor was David Dill.

My research focuses on ways to ensure that computer systems do the right thing. I am particularly interested in theorem proving, decision procedures, invariant detection, and combinational equivalence checking. Recently, I have been working on correct-by-construction software synthesis.

Click for more information on my dissertation about automating correctness proofs of real-world Java implementations of cryptographic algorithms. For that project, I developed a theorem prover and equivalence checker called Axe.