Research

My areas of interesting include automated reasoning, theorem proving, decision procedures, satisfiability (SAT) and satisfiability modulo theories (SMT). My main project is the Lean theorem prover. The Lean project aims to bring the automated and interactive theorem proving worlds together. One of the main goals is to provide a powerful system for reasoning about complex systems and mathematics, and verifying claims about both. You can try Lean on your web browser.

I also work on Z3. Z3 is a very efficient SMT solver, it has builtin support for many useful theories such as: linear real and integer arithmetic, nonlinear real arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools both within Microsoft and elsewhere

Internships

I am always looking for bright interns. If you are interested in an internship at Microsoft Research in one of the topics above, please send me an email. My current focus is the Lean theorem prover.