Leonardo de Moura home about me publications slides research

Slides

Lean related presentations can be found here.
Lost in translation: how easy problems become hard due to bad encodings, Vampire workshop, Berlin, 2015
The Lean Theorem Prover Tutorial, CADE-25 Tutorial, Berlin, 2015
The Lean Theorem Prover, CICM, Washington D.C., 2015
The Lean Theorem Prover, NASA Langley, Virginia, 2015
MCSat: A Model-Constructing Satisfiability Calculus, International Conference on Theory and Applications of Satisfiability Testing, Vienna, 2014 (Power-point version)
Non-linear Arithmetic, SAT/SMT summer school 2014, Vienna, 2014 (Power-point version)
Z3: Logic Engines as a Service, award for “The most influential tool paper in the first 20 years of TACAS”, TACAS 20, Grenoble, France, 2014 (Power-point version)
Arithmetic and Optimization @ MCSAT, Dagstuhl seminar on Deduction and Arithmetic, Germany 2013 (Power-point version)
Model-Driven Decision Procedures for Arithmetic, SYNASC 2013, Romania (invited) (Power-point version)
Internals of SMT Solvers, SAT/SMT Summer School 2013, Espoo, Finland, 2013 (invited) (Power-point version).
Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals, CADE’13, Lake Placid, New York, 2013 (Power-point version).
Decision Methods for Arithmetic, Third Summer School on Formal Techniques, Menlo Park, 2013. Slides: part 1, part 2, part 3, exercises. Power-point slides: part 1, part 2, part 3, exercises
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).
Satisfiability Modulo Theories (SMT): Ideas & Applications, Universita Degli Studi di Milano, Italy, March 2010 (part1, part2, part3, part4, assignment); powerpoint version: (part1, part2, part3, part4)
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](http://mtc.epfl.ch/events/WIN York, UK, powerpoint slides (invited).</li>
Quantifiers in Satisfiability Modulo Theories, [Frontiers of Computational Reasoning](http://www.dcs.qmul.ac.uk/~ohearn/Workshops/Reasonin Cambridge, UK, powerpoint slides.</li>
Quantifiers in Satisfiability Modulo Theories, Univeristy of Manchester, UK powerpoint slides.
Accelerating lemma learning using joins, [LPAR 2008](http://www.qatar.cmu.edu/lpar08/program.sh Doha, Qatar, powerpoint slides.</li>
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](http://www.ijcar.org/2 Sydney, Australia, powerpoint slides.</li>
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).