I'm a Principal Researcher in the RiSE group at
New Lean Theorem Prover (source code)
Z3: Theorem Prover
Slides for my talk at the Dagstuhl seminar on Deduction and Arithmetic.
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.
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),