I'm a Senior Principal Researcher in the RiSE group at
Microsoft Research.
Projects
Lean Theorem Prover
Z3 Theorem Prover
Teaching
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,
(part 1,
part 2,
part 3,
exercises).
- 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
(part 1,
part 2,
part 3,
part 4,
assignment).
- On Designing and Implementing Satisfiability Modulo Theory Solvers,
Summer School 2009: Verification Technology, Systems & Applications, Nancy, France
(lecture 1,
lecture 2).
- 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.