I'm a Principal Researcher in the RiSE group at Microsoft Research.


New Lean Theorem Prover (source code)

Z3: Theorem Prover


The TACAS conference (Tools and Algorithms for the Construction and Analysis of Systems) has given an award for "The most influential tool paper in the first 20 years of TACAS" to the Z3 paper: Z3: An Efficient SMT Solver. 14th International Conference, TACAS 2008, vol. 4963 of Lecture Notes in Computer Science.


I really enjoy teaching. Here is a list of courses I have taught in the past.

Professional Activities

IJCAR 2014 (PC), CADE 24 (PC), TACAS'13 (PC), SAT'13 (PC), NFM'13 (PC), SBMF'13 (PC co-chair), POPL'13 (ERC), SAT'12 (PC), VSTTE'12 (PC), FM'12 (PC), CADE'11 (PC), SMT'11 (PC), PxTP'11 (PC), SAT'11 (PC), LICS'11 (PC), EMS+QMS 2010 (Panelist), SMT'10 (PC), TACAS'10 (PC), FMCAD'09 (PC), SMT'09 (PC), AFM'09 (PC), BPR'09 (PC), Beyond-SAT'09 (PC), FroCoS'09 (PC), AFM'08 (PC), IJCAR'08 (tutorial: SMT in program verification), SMT'08 (co-chair), SAT'08 (PC), BPR'08 (PC), AFM'07 (PC), SMT'07 (PC), SAT'07 (PC), FMDCAD'06 (tutorial chair, PC), PDPAR'06 (PC), SMT-COMP'06 (organizer), SMT-COMP'05 (organizer).