Leonardo de Moura
Microsoft Research
- Senior Researcher in the RiSE group at Microsoft Research.
- Tel.: (425) 421-6987
- Fax: (425) 936-7329
- Email: leonardo AT microsoft DOT com
- Address: One Microsoft Way, Redmond, WA, 98052
Professional interests:
SMT solvers, Decision Procedures, Theorem Proving, Static Analysis.
News
Projects
Publications
- Real Algebraic Strategies for MetiTarski Proofs, Grant Olney Passmore, Lawrence C. Paulson and Leonardo de Moura, Conference on Intelligent Computer Mathematics (CICM/AISC), 2012.
- Solving non-linear arithmetic, Dejan Jovanovic and Leonardo de Moura, IJCAR, Manchester, UK, 2012. Extended Version.
- 6 Years of SMT-COMP, Clark Barrett, Morgan Deters, Leonardo de Moura, Albert Oliveras and Aaron Stump, Journal of Automated Reasoning, 2012.
- Satisfiability Modulo Theories: Introduction and Applications (html version), Leonardo de Moura and Nikolaj Bjorner, Communications of the ACM, September, 2011.
- Cutting to the Chase: Solving Linear Integer Arithmetic, Dejan Jovanovic and Leonardo de Moura, CADE, Wroclaw, Poland, 2011.
- muZ: An Efficient Engine for Fixed Points with Constraints, Krystof Hoder, Nikolaj Bjorner, and Leonardo de Moura, CAV, Snowbird, Utah, 2011.
- On deciding satisfiability by theorem proving with speculative inferences., Maria Paola Bonacina, Christopher A. Lynch and Leonardo de Moura, Journal of Automated Reasoning, doi=10.1007/s10817-010-9213-y, 2011.
- Applications and Challenges in Satisfiability Modulo Theories. Leonardo de Moura and Nikolaj Bjørner. To appear in the First EasyChair Volume on WING (Workshop on Invariant Generation).
- Symbolic Automata Constraint Solving, Margus Veanes, Nikolaj Bjorner, and Leonardo de Moura, LPAR, Yogyakarta, Indonesia, 2010.
- Efficiently Solving Quantified Bit-Vector Formula, Christoph Wintersteiger, Youssef Hamadi and Leonardo de Moura, FMCAD, Lugano, Switzerland, 2010.
- Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development, Leonardo de Moura, Nikolaj Bjørner, IJCAR, Edinburgh, Scotland, 2010.
- Grobner Basis Construction Algorithms Based on Theorem Proving Saturation Loops, Grant Olney Passmore, Leonardo de Moura and Paul Jackson, submitted to the proceedings for "Decision Procedures in Software, Hardware and Bioware" Seminar at Dagstuhl, Germany, 2010.
- Generalized and Efficient Array Decision Procedures, Leonardo de Moura, Nikolaj Bjørner, FMCAD, Austin TX, 2009. Extended version: Technical report MSR-TR-2009-121.
- Satisfiability Modulo Theories: An Appetizer, Leonardo de Moura, Nikolaj Bjørner, invited paper to SBMF 2009, Gramado, Brazil.
- Superfluous S-polynomials in Strategy-Independent Grobner Bases, Grant Olney Passmore, Leonardo de Moura, 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), Timisoara, Romania, 2009.
- On Locally Minimal Nullstellensatz Proofs, Leonardo de Moura, Grant Olney Passmore, SMT'09. Extended version: Techical report MSR-TR-2009-90.pdf.
- Universality of Polynomial Positivity and a Variant of Hilbert's 17th Problem, Grant Olney Passmore, Leonardo de Moura, ADDCT'09.
- Z310: Applications, Enablers, Challenges and Directions, Nikolaj Bjørner, Leonardo de Moura, invited paper to CFV 2009.
- On deciding satisfiability by DPLL(Gamma+T) and unsound theorem proving, Maria Paola Bonacina, Christopher Lynch and Leonardo de Moura, 22nd International Conference on Automated Deduction (CADE-22), Montreal, Canada, 2009.
- Complete instantiation for quantified SMT formulas, Yeting Ge and Leonardo de Moura, Conference on Computer Aided Verification (CAV 2009), Grenoble, France, 2009.
- A Concurrent Portfolio Approach to SMT Solving, Christoph M. Wintersteiger, Youssef Hamadi and Leonardo de Moura, Conference on Computer Aided Verification (CAV 2009), Grenoble, France, 2009.
- Deciding Effectively Propositional Logic with Equality, Ruzica Piskac, Leonardo de Moura, and Nikolaj Bjørner, Technical Report: MSR-TR-2008-181
- Accelerating Lemma Learning using Joins - DPPL(Join), Nikolaj Bjørner, Bruno Dutertre and Leonardo de Moura, Short paper at LPAR 2008, Doha.
- Proofs and Refutations, and Z3, Leonardo de Moura and Nikolaj Bjørner, IWIL 2008.
- Satisfiability Modulo Bit-precise Theories for Program Exploration, Nikolaj Bjørner, Leonardo de Moura and Nikolai Tillmann, Invited workshop paper, CFV 2008.
- Deciding Effectively Propositional Logic using DPLL and substitution sets, Leonardo de Moura and Nikolaj Bjørner, International Joint Conference on Automated Reasoning (IJCAR), Sydney, Australia, 2008.
- Engineering DPLL(T) + Saturation, Leonardo de Moura and Nikolaj Bjørner, International Joint Conference on Automated Reasoning (IJCAR), Sydney, Australia, 2008.
- Z3: An Efficient SMT Solver, Leonardo de Moura and Nikolaj Bjørner, Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Budapest, Hungary, 2008.
- Relevancy Propagation, Leonardo de Moura and Nikolaj Bjørner, MSR Technical Note, October 2007.
- Efficient E-matching for SMT solvers, Leonardo de Moura and Nikolaj Bjørner, Conference on Automated Deduction (CADE), Bremen, Germany, 2007.
- Model-based Theory Combination, Leonardo de Moura and Nikolaj Bjørner, Workshop on Satisfiability Modulo Theories (SMT), Berlin, Germany, 2007.
- Design and Results of the Second Satisfiability Modulo Theories Competition (SMT-COMP 2006), Clark Barrett, Leonardo de Moura, and Aaron Stump, Formal Methods in System Design, 2007. To appear.
- A Tutorial on Satisfiability Modulo Theories, Leonardo de Moura, Bruno Dutertre, and Natarajan Shankar, Conference on Computer Aided Verification (CAV), Berlin, Germany, 2007.
- A Fast Linear-Arithmetic Solver for DPLL(T), Bruno Dutertre and Leonardo de Moura, Conference on Computer Aided Verification (CAV), Seattle, WA, 2006.
- Integrating Simplex with DPLL(T), Bruno Dutertre and Leonardo de Moura, SRI Technical Report: SRI-CSL-06-01.
- Design and Results of the 1st Satisfiability Modulo Theories Competition (SMT-COMP 2005), Clark Barrett, Leonardo de Moura, and Aaron Stump, Journal of Automated Reasoning (JAR)
- Integrating Verification Components, Leonardo de Moura, Sam Owre, Harald Ruess, John Rushby, and Natarajan Shankar, Invited position paper for Verified Software: Theories, Tools, Experiments, Zurich, Switzerland, October 2005
- Automated Test Generation with SAL, Gregoire Hamon, Leonardo de Moura, and John Rushby, CSL Technical Note, January 2005.
- Generating Efficient Test Sets with a Model Checker, Gregoire Hamon, Leonardo de Moura, and John Rushby, SEFM'04, Beijing, China, September 2004.
- Justifying Equality, Leonardo de Moura, Harald Ruess and Natarajan Shankar, PDPAR 2004, Cork, Ireland, July 2004.
- SAL 2, Leonardo de Moura, Sam Owre, Harald Ruess, John Rushby, N. Shankar, Maria Sorea, and Ashish Tiwari, Computer-Aided Verification, CAV '2004.
- An Experimental Evaluation of Ground Decision Procedures, Leonardo de Moura and Harald Ruess, Computer-Aided Verification, CAV '2004.
- The ICS decision procedures for embedded deduction, Leonardo de Moura, Harald Ruess, Natarajan Shankar, and John Rushby, IJCAR 2004, Cork, Ireland, July 2004.
- From Simulation to Verification (and Back), Harald Ruess and Leonardo de Moura, 2003 Winter Simulation Conference.
- Embedded Deduction With ICS, Leonardo de Moura, Harald Ruess, John Rushby, and Natarajan Shankar, NSA's Third High Confidence Software and Systems Conference, Baltimore, MD, 2003.
- Bounded Model Checking and Induction: From Refutation to Verification, Leonardo de Moura, Harald Ruess, and Maria Sorea, Computer-Aided Verification, CAV '2003.
- Lazy Theorem Proving for Bounded Model Checking over Infinite Domains, Leonardo de Moura, Harald Ruess, and Maria Sorea, 18th International Conference on Automated Deduction, CADE'2002.
- Lemmas on Demand for Satisfiability Solvers, Leonardo de Moura and Harald Ruess, Fifth International Symposium on the Theory and Applications of Satisfiability Testing, SAT'02.
- Clone Detection Using Abstract Syntax Trees, Ira Baxter, Andrew Yahin, Leonardo de Moura, Marcelo Sant'Anna, Lorraine Bier, International Conference on Maintenance, ICSM'98.
Slides
- 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, Invited talk at IJCAR'2010, Edinburgh, UK, 2010 (invited)
- Satisfiability with and without theories, Invited tutorial at KR'2010, Toronto, Canada, 2010 (invited)
- Generalized and Efficient Array Decision Procedures, FMCAD, 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, York, UK (Powerpoint Slides) (invited)
- Quantifiers in Satisfiability Modulo Theories, Frontiers of Computational Reasoning, Cambridge, UK (Powerpoint Slides).
- Quantifiers in Satisfiability Modulo Theories, Univeristy of Manchester, UK (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) (invited)
- Invited Tutorial: Applications of SMT solvers in Software Verification, VSTTE'08, Toronto, Canada 2008 (Powerpoint Slides).
- Experiments in Software Verification using SMT solvers, VS Experiments'08, Toronto, Canada 2008 (Powerpoint Slides) (invited)
- Engineering DPLL(T) + Saturation (PDF), IJCAR'08, Sydney, Australia 2008 (Powerpoint Slides) (invited)
- SMT solvers in Program Analysis and Verification (PDF), Tutorial at IJCAR'08, Sydney, Australia 2008 (Powerpoint slides).
- SMT Solvers: Theory and Implementation, Summer School on Logic and Theorem Proving in Programming Languages, Oregon 2008 (exercises) (invited)
- SMT@Microsoft (PDF), Institute for Formal Models and Verification at the Johannes Kepler University, Linz, Austria, 2008 (Powerpoint Slides).
- Z3: An Efficient SMT Solver (PDF), TACAS, Budapest, Hungary, 2008 (Powerpoint Slides).
- Z3: An Efficient SMT Solver, McMaster University Hamilton, CA, 2007.
- SMT@Microsoft, AFM, Atlanta, 2007 (invited)
- SMT@Microsoft, Intel, Portland, 2007.
- Developing Efficient SMT Solvers, ESARLT, Bremen, Germany, 2007 (invited)
- SMT solvers: Introduction & Applications, University of Cambridge, UK, 2007.
- Z3: An Efficient SMT solver, MS Research Cambridge, UK, 2007.
- Efficient E-matching for SMT solvers, CADE, Bremen, Germany, 2007.
- Z3 0.1: An Efficient SMT solver, SMT-COMP, Berlin, Germany, 2007.
- Model-based Theory Combination, SMT, Berlin, Germany, 2007.
- Developing Efficient SMT Solvers, Carnegie Mellon University, Pittsburgh, 2007 (invited)
- Tutorial on SMT solvers, FMCAD, San Jose, 2006 (invited)
Professional Activities
- SAT'12 (PC), VSTTE'12 (PC), FM'12 (PC), CADE'11 (PC), SMT'11 (PC), PxTP'11 (PC), SAT'11 (PC), LICS'11 (PC), EMS+QMS 2010 (Panelist), SMT'10 (PC),
- TACAS'10 (PC), FMCAD'09 (PC), SMT'09 (PC), AFM'09 (PC), BPR'09 (PC), Beyond-SAT'09 (PC),
- FroCoS'09 (PC), AFM'08 (PC), IJCAR'08 (tutorial: SMT in program verification), SMT'08 (co-chair),
- SAT'08 (PC), BPR'08 (PC), AFM'07 (PC), SMT'07 (PC), SAT'07 (PC),
- FMDCAD'06 (tutorial chair, PC), PDPAR'06 (PC), SMT-COMP'06 (organizer), SMT-COMP'05 (organizer).
Links
Courses
- 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.