Publications

[1]
Dejan Jovanović, Clark Barrett, and Leonardo de Moura. The design and implementation of the model constructing satisfiability calculus. In Proceedings of 13th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2013, 20-23 October 2013, Porland, Oregon, USA, 2013. [ bib | .pdf ]
[2]
Leonardo de Moura and Grant Passmore. Computation in real closed infinitesimal and transcendental extensions of the rationals. In Automated Deduction - CADE-24, 24th International Conference on Automated Deduction, Lake Placid, New York, June 9-14, 2013, Proceedings, 2013. [ bib | http ]
[3]
Dejan Jovanović and Leonardo de Moura. Cutting to the chase: Solving linear integer arithmetic (to appear). Journal Automated Reasoning, 2013. [ bib | .pdf ]
[4]
Leonardo de Moura and Grant Passmore. The Strategy Challenge in SMT Solving, volume 7788 of Lecture Notes in Artificial Intelligence. Springer, 2013. [ bib | .pdf ]
[5]
Leonardo de Moura and Dejan Jovanović. A model-constructing satisfiability calculus. In 14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI, Rome, Italy, 2013, 2013. [ bib | .pdf ]
[6]
Grant Olney Passmore, Lawrence C. Paulson, and Leonardo de Moura. Real algebraic strategies for MetiTarski proofs. In Intelligent Computer Mathematics - 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings, volume 7362 of Lecture Notes in Computer Science, pages 358-370. Springer, 2012. [ bib | .pdf ]
[7]
Dejan Jovanović and Leonardo de Moura. Solving non-linear arithmetic. In Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, volume 7364 of Lecture Notes in Computer Science, pages 339-354. Springer, 2012. [ bib | .pdf ]
[8]
Dejan Jovanović and Leonardo de Moura. Solving non-linear arithmetic. Technical Report MSR-TR-2012-20, Microsoft Research, 2012. [ bib | http ]
[9]
Clark Barrett, Morgan Deters, Leonardo de Moura, Albert Oliveras, and Aaron Stump. 6 Years of SMT-COMP. Journal of Automated Reasoning, 2012. [ bib | http ]
[10]
Christoph Wintersteiger, Youssef Hamadi, and Leonardo de Moura. Efficiently solving quantified bit-vector formulas. Formal Methods in System Design, 2012. [ bib | http | .pdf ]
[11]
Nikolaj Bjørner and Leonardo de Moura. Tractability and Modern Satisfiability Modulo Theories Solvers. In Handbook of Tractability. Cambridge University Press, 2012. [ bib | .pdf ]
[12]
Krystof Hoder, Nikolaj Bjørner, and Leonardo de Moura. muZ - an efficient engine for fixed points with constraints. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 457-462, 2011. [ bib | .pdf ]
[13]
Leonardo de Moura and Nikolaj Bjørner. Satisfiability modulo theories: introduction and applications. Commun. ACM, 54(9):69-77, 2011. [ bib | http ]
[14]
Dejan Jovanović and Leonardo de Moura. Cutting to the chase solving linear integer arithmetic. In Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, volume 6803 of Lecture Notes in Computer Science, pages 338-353. Springer, 2011. [ bib | .pdf ]
[15]
Maria Paola Bonacina, Christopher Lynch, and Leonardo de Moura. On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reasoning, 47(2):161-189, 2011. [ bib | .pdf ]
[16]
Leonardo de Moura and Nikolaj Bjørner. Bugs, moles and skeletons: Symbolic reasoning for software development. In Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings, volume 6173 of Lecture Notes in Computer Science, pages 400-411. Springer, 2010. [ bib | .pdf ]
[17]
Margus Veanes, Nikolaj Bjørner, and Leonardo de Moura. Symbolic automata constraint solving. In Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings, volume 6397 of Lecture Notes in Computer Science, pages 640-654, 2010. [ bib | .pdf ]
[18]
Ruzica Piskac, Leonardo de Moura, and Nikolaj Bjørner. Deciding effectively propositional logic using DPLL and substitution sets. J. Autom. Reasoning, 44(4):401-424, 2010. [ bib | http ]
[19]
Christoph M. Wintersteiger, Youssef Hamadi, and Leonardo de Moura. Efficiently solving quantified bit-vector formulas. In Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23, pages 239-246. IEEE, 2010. [ bib | .pdf ]
[20]
Leonardo de Moura and Nikolaj Bjørner. Generalized, efficient array decision procedures. In Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA, pages 45-52. IEEE, 2009. [ bib | .pdf ]
[21]
Nikolaj Bjørner and Leonardo de Moura. Tapas: Theory combinations and practical applications. In Formal Modeling and Analysis of Timed Systems, 7th International Conference, FORMATS 2009, Budapest, Hungary, September 14-16, 2009. Proceedings, volume 5813 of Lecture Notes in Computer Science, pages 1-6. Springer, 2009. [ bib | http ]
[22]
Leonardo de Moura and Nikolaj Bjørner. Satisfiability modulo theories: An appetizer. In Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009, Revised Selected Papers, volume 5902 of Lecture Notes in Computer Science, pages 23-36. Springer, 2009. [ bib | .pdf ]
[23]
Maria Paola Bonacina, Christopher Lynch, and Leonardo de Moura. On deciding satisfiability by DPLL(Γ+T) and unsound theorem proving. In Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, volume 5663 of Lecture Notes in Computer Science, pages 35-50. Springer, 2009. [ bib | .pdf ]
[24]
Yeting Ge and Leonardo de Moura. Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science, pages 306-320. Springer, 2009. [ bib | .pdf ]
[25]
Yeting Ge and Leonardo de Moura. Complete instantiation for quantified formulas in satisfiabiliby modulo theories (extended version). 2009. [ bib | .pdf ]
[26]
Christoph M. Wintersteiger, Youssef Hamadi, and Leonardo de Moura. A concurrent portfolio approach to SMT solving. In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science, pages 715-720. Springer, 2009. [ bib | .pdf ]
[27]
Grant Olney Passmore and Leonardo de Moura. Superfluous S-polynomials in strategy-independent groebner bases. In 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2009, Timisoara, Romania, September 26-29, 2009, pages 45-53. IEEE Computer Society, 2009. [ bib | .pdf ]
[28]
Nikolaj Bjørner and Leonardo de Moura. z310: Applications, enablers, challenges and directions. In Sixth International Workshop on Constraints in Formal Verification Grenoble, France, 2009. [ bib | .pdf ]
[29]
Leonardo de Moura and Grant Olney Passmore. On locally minimal nullstellensatz proofs. In 7th International Workshop on Satisfiability Modulo Theories, SMT, Montreal, Canada, 2009. [ bib | .pdf ]
[30]
Leonardo de Moura and Grant Olney Passmore. On locally minimal nullstellensatz proofs. Technical Report MSR-TR-2009-90, Microsoft Research, 2009. [ bib | .pdf ]
[31]
Grant Olney Passmore and Leonardo de Moura. Universality of polynomial positivity and a variant of Hilbert's 17th problem. In Automated Deduction: Decidability, Complexity, Tractability, ADDCT'09, Montreal, Canada, 2009. [ bib | .pdf ]
[32]
Ruzica Piskac, Leonardo de Moura, and Nikolaj Bjørner. Deciding effectively propositional logic with equality. Technical Report MSR-TR-2008-181, Microsoft Research, 2008. [ bib | http ]
[33]
Leonardo de Moura and Nikolaj Bjørner. Deciding effectively propositional logic using DPLL and substitution sets. In Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lecture Notes in Computer Science, pages 410-425. Springer, 2008. [ bib | .pdf ]
[34]
Leonardo de Moura and Nikolaj Bjørner. Engineering DPLL(T) + Saturation. In Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lecture Notes in Computer Science, pages 475-490. Springer, 2008. [ bib | .pdf ]
[35]
Leonardo de Moura and Nikolaj Bjørner. Proofs and refutations, and Z3. In Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, November 22, 2008, volume 418 of CEUR Workshop Proceedings. CEUR-WS.org, 2008. [ bib | .pdf ]
[36]
Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. [ bib | .pdf ]
[37]
Leonardo de Moura and Nikolaj Bjørner. Model-based theory combination. Electr. Notes Theor. Comput. Sci., 198(2):37-49, 2008. [ bib | .pdf ]
[38]
Nikolaj Bjørner, Bruno Dutertre, and Leonardo de Moura. Accelerating lemma learning using joins - DPPL(Join). In 15th International Conference on Logic for Programming Artificial Intelligence and Reasoning, LPAR'08, 2008. [ bib | .pdf ]
[39]
Nikolaj Bjørner, Leonardo de Moura, and Nikolai Tillmann. Satisfiability modulo bit-precise theories for program exploration. In Fifth International Workshop on Constraints in Formal Verification, (CFV'08), Sydney, Australia, 2008. [ bib | .pdf ]
[40]
Leonardo de Moura and Nikolaj Bjørner. Efficient E-Matching for SMT solvers. In Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings, volume 4603 of Lecture Notes in Computer Science, pages 183-198. Springer, 2007. [ bib | .pdf ]
[41]
Leonardo de Moura, Bruno Dutertre, and Natarajan Shankar. A tutorial on satisfiability modulo theories. In Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, volume 4590 of Lecture Notes in Computer Science, pages 20-36. Springer, 2007. [ bib | http ]
[42]
Clark W. Barrett, Leonardo de Moura, and Aaron Stump. Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006). Formal Methods in System Design, 31(3):221-239, 2007. [ bib | .pdf ]
[43]
Leonardo de Moura and Nikolaj Bjørner. Relevancy propagation. Technical Report MSR-TR-2007-140, Microsoft Research, 2007. [ bib | .pdf ]
[44]
Bruno Dutertre and Leonardo de Moura. A fast linear-arithmetic solver for DPLL(T). In Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4144 of Lecture Notes in Computer Science, pages 81-94. Springer, 2006. [ bib | .pdf ]
[45]
Bruno Dutertre and Leonardo de Moura. The Yices SMT solver. Technical report, SRI International, 2006. [ bib | .pdf ]
[46]
Bruno Dutertre and Leonardo de Moura. Integrating simplex with DPLL(T). Technical report, SRI International, 2006. [ bib | .pdf ]
[47]
Clark Barrett, Leonardo de Moura, and Aaron Stump. Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005). Journal of Automated Reasoning, 35(4):373-390, November 2005. [ bib | DOI | .pdf ]
[48]
Clark W. Barrett, Leonardo de Moura, and Aaron Stump. SMT-COMP: Satisfiability modulo theories competition. In Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings, volume 3576 of Lecture Notes in Computer Science, pages 20-23. Springer, 2005. [ bib | .pdf ]
[49]
Leonardo de Moura, Harald Rueß, and Natarajan Shankar. Justifying equality. Electr. Notes Theor. Comput. Sci., 125(3):69-85, 2005. [ bib | .pdf ]
[50]
Grégoire Hamon, Leonardo de Moura, and John Rushby. Automated test generation with SAL. Technical report, SRI International, 2005. CSL Technical Note. [ bib | .pdf ]
[51]
Leonardo de Moura, Sam Owre, Harald Rueß, John Rushby, and Natarajan Shankar. Integrating verification components. In In Verified Software: Theories, Tools, Experiments, 2005. [ bib | .pdf ]
[52]
Leonardo de Moura and Harald Rueß. An experimental evaluation of ground decision procedures. In Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings, volume 3114 of Lecture Notes in Computer Science, pages 162-174. Springer, 2004. [ bib | .pdf ]
[53]
Leonardo de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar, Maria Sorea, and Ashish Tiwari. SAL 2. In Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings, volume 3114 of Lecture Notes in Computer Science, pages 496-500. Springer, 2004. [ bib | .pdf ]
[54]
Leonardo de Moura, Sam Owre, Harald Rueß, John M. Rushby, and Natarajan Shankar. The ICS decision procedures for embedded deduction. In Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings, volume 3097 of Lecture Notes in Computer Science, pages 218-222. Springer, 2004. [ bib | .pdf ]
[55]
Grégoire Hamon, Leonardo de Moura, and John M. Rushby. Generating efficient test sets with a model checker. In 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 28-30 September 2004, Beijing, China, pages 261-270. IEEE Computer Society, 2004. [ bib | .pdf ]
[56]
Leonardo de Moura, Harald Rueß, and Maria Sorea. Bounded model checking and induction: From refutation to verification. In Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, volume 2725 of Lecture Notes in Computer Science, pages 14-26. Springer, 2003. [ bib | .pdf ]
[57]
Harald Rueß and Leonardo de Moura. From simulation to verification (and back). In Proceedings of the 35th Winter Simulation Conference: Driving Innovation, New Orleans, Louisiana, USA, December 7-10, 2003, pages 888-896. ACM, 2003. [ bib | .pdf ]
[58]
Leonardo de Moura, Harald Rueß, John Rushby, and Natarajan Shankar. Embedded deduction with ICS, 2003. [ bib | .pdf ]
[59]
Leonardo de Moura, Harald Rueß, and Maria Sorea. Lazy theorem proving for bounded model checking over infinite domains. In Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings, volume 2392 of Lecture Notes in Computer Science, pages 438-455. Springer, 2002. [ bib | .pdf ]
[60]
Leonardo de Moura and Harald Rueß. Lemmas on demand for satisfiability solvers. In Symposium on the Theory and Applications of Satisfiability Testing (SAT'02), Cincinnati, USA, 2002. [ bib | .pdf ]
[61]
Ira D. Baxter, Andrew Yahin, Leonardo de Moura, Marcelo Sant'Anna, and Lorraine Bier. Clone detection using abstract syntax trees. In International Conference on Software Maintenance (ICSM'98), Bethesda, Maryland, USA, pages 368-377, 1998. [ bib | .pdf ]

This file was generated by bibtex2html 1.96.