Leonardo de Moura

Microsoft Research

Researcher in the Software Reliability Research 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.

Projects

Z3: SMT Solver

Publications

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.
Z3¹⁰: 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.