My areas of interesting include automated reasoning, theorem proving, decision procedures, satisfiability (SAT) and satisfiability modulo theories (SMT). My main project is the Z3 theorem prover. 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


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.

On-line Tutorials

I have written many on-line tutorials about Z3. The tutorials contain many examples that can be tried from your browser. You do not have to install Z3 to try it. If you like Python, you should try Z3Py.

The Z3Py tutorials are temporarily offline because of security issues. They will remain offline until these issues are fixed.

Trying Z3 On-line