Slides

Slides

Introductory

• Z3: An Efficient SMT Solver (PDF), TACAS, Budapest, Hungary, 2008 (Powerpoint Slides).
• SMT@Microsoft, Max Planck Institut Informatik, Germany, 2009.
• Satisfiability Modulo Theories: An Appetizer, SBMF 2009, Gramado, Brazil (Powerpoint Slides)

Tutorials and Summer Schools

• First Summer School on Formal Techniques, Menlo Park, 2011.
• Satisfiability Modulo Theories (SMT): Ideas and Applications, Universita Degli Studi di Milano, Italy, March 2010 (part 1, part 2, part 3, part 4, assignment).
• Satisfiability with and without theories, Invited tutorial at KR'2010, Toronto, Canada, 2010
• On Designing and Implementing Satisfiability Modulo Theory Solvers, Summer School 2009: Verification Technology, Systems and Applications, Nancy, France (lecture 1, lecture 2)
• Invited Tutorial: Applications of SMT solvers in Software Verification, VSTTE'08, Toronto, Canada 2008 (Powerpoint Slides)
• Tutorial on SMT solvers in program analysis and Verification at Microsoft, Presented at IJCAR, Australia 2008 url:(PDF) (PowerPoint).
• SMT Solvers: Theory and Implementation, Summer School on Logic and Theorem Proving in Programming Languages, Oregon 2008.
• SMT Solvers in Program Verification and Analysis, MSR India Summer School on Programming Languages, Analysis and Verification, Bangalore, June 2008. Lecture 1 Lecture 2 Lecture 3 Lecture 4 Lecture 5 Lab Exercises. Student solutions: Ashish Sharma.
• Tutorial on SMT solvers, FMCAD 2006.

Technical presentations

• SMT: Techniques, Hurdles, Applications, First International SAT/SMT Solver Summer School 2011, MIT, 2011
• Orchestrating Decision Engines, CP'2011, Perugia, Italy, 2011
• Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development, Invited talk at IJCAR'2010, Edinburgh, UK, 2010
• Generalized and Efficient Array Decision Procedures, FMCAD, Austin TX, 2009.
• Applications and Challenges in Satisfiability Modulo Theories, WING 2009, York, England (Powerpoint Slides).
• [Complete Instantiation for Quantified Formulas in SMT](http://research.microsoft.com/~leonardo/cav2009.pdf(, CAV 2009, Grenoble, France.
• Quantifiers in Satisfiability Modulo Theories, Frontiers of Computational Reasoning, Cambridge, England (Powerpoint Slides).
• Accelerating lemma learning using joins, LPAR 2008, Doha, Qatar (Powerpoint Slides).
• Software Verification and Testing, NSF Workshop on Symbolic Computation for Constraint Satisfaction Problems, Virginia, 2008 (Powerpoint Slides).
• Experiments in Software Verification using SMT solvers, VS Experiments'08, Toronto, Canada 2008 (Powerpoint Slides).
• Engineering DPLL(T) + Saturation (PDF), IJCAR'08, Sydney, Australia 2008 (Powerpoint Slides).
• Efficient E-matching for SMT solvers, CADE 2007.
• Model-based Theory Combination, SMT 2007.
• Developing Efficient SMT Solvers, CMU 2007.