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


New Lean Theorem Prover

Z3: Theorem Prover


Theorem Proving in Lean (PDF)

Tutorial on Lean at CADE 2015

Interactive Theorem Proving course at CMU using Lean

Invited talk at CICM 2015

Z3 is now open source (MIT License)


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

Professional Activities

SAT 2015 (PC), NFM 2015 (PC), CPP 2015 (PC), SMT 2015 (PC), 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).