I'm a Principal Researcher in the RiSE group at
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.
- Tools and Algorithms in Real Algebraic Geometry, University of Milan, Italy, May 2013.
- Decision Methods for Arithmetic, Third Summer School on Formal Techniques, Menlo Park, 2013,
- Second Summer School on Formal Techniques, Menlo Park, 2012.
- First Summer School on Formal Techniques, Menlo Park, 2011.
- Satisfiability Modulo Theories (SMT): Ideas & Applications, Universita Degli Studi di Milano, Italy, March 2010
- On Designing and Implementing Satisfiability Modulo Theory Solvers,
Summer School 2009: Verification Technology, Systems & Applications, Nancy, France
- SMT Solvers: Theory and Implementation,
Summer School on Logic and Theorem Proving in Programming Languages,
Oregon 2008 (exercises).
- CS359: Little Engines of Proof, Stanford University, Fall 2003.
SAT 2015 (PC),
NFM 2015 (PC),
CPP 2015 (PC),
SMT 2015 (PC),
IJCAR 2014 (PC),
CADE 24 (PC),
SBMF'13 (PC co-chair),
EMS+QMS 2010 (Panelist),
IJCAR'08 (tutorial: SMT in program verification),
FMDCAD'06 (tutorial chair, PC),