Slides

• A Model-Constructing Satisfiability Calculus, VMCAI'13, Rome, Italy, 2013 (Power-point version).
• Tutorial on SMT, Natal, Brazil, 2012 (Z3Py Examples).
• The Strategy Challenge in SMT Solving (joint talk with Grant Passmore), Part I Part II, IWS2012, Manchester, UK, 2012.
• Regression Tests and the Inventor's Dilemma, COMPARE 2012, Manchester, UK, 2012 (invited).
• Solving nonlinear arithmetic, IJCAR 2012, Manchester, UK, 2012.
• Quantifiers in SMT solvers, SAT/SMT Summer School 2012, Trento, Italy, 2012 (invited).
• Orchestrating Decision Engines, CP 2011, Perugia, Italy, 2011 (invited).
• Orchestrating Decision Engines, University of Verona Verona, Italy, 2011.
• Tactics, Tacticals and SMT, FBK, Trento, Italy, 2011.
• SMT@Microsoft, FMICS 2011, Trento, Italy, 2011 (invited).
• SMT: Techniques, Hurdles, Applications, First International SAT/SMT Solver Summer School 2011, MIT, 2011 (invited).
• Orchestrating Decision Engines, Deduction at Scale Seminar, Germany, 2011 (invited).
• Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development, IJCAR 2010, Edinburgh, UK, 2010 (invited).
• Satisfiability with and without theories, KR 2010, Toronto, Canada, 2010 (invited).
• Generalized and Efficient Array Decision Procedures, FMCAD 2009, Austin TX, 2009.
• SMT@Microsoft, New York University, New York, 2009.
• SMT@Microsoft, Max Planck Institut Informatik, Germany, 2009.
• On Designing and Implementing Satisfiability Modulo Theory Solvers, Summer School 2009: Verification Technology, Systems & Applications, Nancy, France, lecture 1, lecture 2, (invited).
• SMT@Microsoft, Midwest Verification Day, Iowa, 2009, powerpoint slides, (invited).
• Satisfiability Modulo Theories: A Calculus of Computation, PUC-Rio, Rio de Janeiro, Brazil, powerpoint slides.
• Satisfiability Modulo Theories: An Appetizer, SBMF 2009, Gramado, Brazil, powerpoint slides, (invited).
• Complete Instantiation for Quantified Formulas in SMT, CAV 2009, Grenoble, France, powerpoint slides.
• Applications and Challenges in Satisfiability Modulo Theories, WING 2009 (invited).
• Quantifiers in Satisfiability Modulo Theories, Frontiers of Computational Reasoning.
• Quantifiers in Satisfiability Modulo Theories, Univeristy of Manchester, UK powerpoint slides.
• Accelerating lemma learning using joins, LPAR 2008.
• Software Verification and Testing, NSF Workshop on Symbolic Computation for Constraint Satisfaction Problems, Virginia, 2008, powerpoint slides, (invited).
• Tutorial: Applications of SMT solvers in Software Verification, VSTTE 2008, Toronto, Canada, powerpoint slides, (invited).
• Experiments in Software Verification using SMT solvers, VS Experiments 2008, Toronto, Canada, powerpoint slides, (invited).
• Engineering DPLL(T) + Saturation, IJCAR 2008, Sydney, Australia, powerpoint slides.
• SMT solvers in Program Analysis and Verification, Tutorial at IJCAR 2008.
• SMT Solvers: Theory and Implementation, Summer School on Logic and Theorem Proving in Programming Languages, Oregon, (invited).
• SMT@Microsoft, Institute for Formal Models and Verification at the Johannes Kepler University, Linz, Austria, powerpoint slides.
• Z3: An Efficient SMT Solver, TACAS 2008, Budapest, Hungary, powerpoint slides.
• Z3: An Efficient SMT Solver, McMaster University, Hamilton, Canada.
• SMT@Microsoft, AFM 2007, Atlanta, (invited).
• SMT@Microsoft, Intel, Portland.
• Developing Efficient SMT Solvers, ESARLT 2007, Bremen, Germany, (invited).
• Z3: An Efficient SMT Solver, MS Research Cambridge, UK.
• Efficient E-matching for SMT solvers, CADE 2007, Bremen, Germany.
• Z3 0.1: An Efficient SMT solver, SMT-COMP 2007, Berlin, Germany.
• Model-based Theory Combination, SMT 2007, Berlin, Germany.
• Developing Efficient SMT Solvers, Carnegie Mellon University, Pittsburgh, (invited).
• Tutorial on SMT solvers, FMCAD 2006, San Jose, (invited).

Leonardo de Moura
Principal Researcher in the RiSE group at Microsoft Research
leonardo@microsoft.com

Stackoverflow
Facebook

Tweet