Publications

[1]

Sebastian Ullrich and Leonardo de Moura. ‘do’ unchained: Embracing local imperativity in a purely functional language (functional pearl). Proc. ACM Program. Lang., 6(ICFP), aug 2022. [ bib | DOI | http | .pdf ]

Keywords: Lean, functional programming, interactive theorem proving

[2]

Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction -- CADE 28, pages 625--635, Cham, 2021. Springer International Publishing. [ bib | .pdf ]

[3]

Alex Reinking, Ningning Xie, Leonardo de Moura, and Daan Leijen. Perceus: Garbage free reference counting with reuse. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, page 96–111, New York, NY, USA, 2021. Association for Computing Machinery. [ bib | DOI | http | .pdf ]

Keywords: Reference Counting, Handlers, Algebraic Effects

[4]

Daniel Selsam, Sebastian Ullrich, and Leonardo de Moura. Tabled typeclass resolution, 2020. [ bib | arXiv | .pdf ]

[5]

Sebastian Ullrich and Leonardo de Moura. Beyond notations: Hygienic macro expansion for theorem proving languages. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, pages 167--182, Cham, 2020. Springer International Publishing. [ bib | .pdf ]

[6]

Sebastian Ullrich and Leonardo de Moura. Counting immutable beans: Reference counting optimized for purely functional programming [in press]. In 31st Symposium on Implementation and Application of Functional Languages, 2019. [ bib | .pdf ]

[7]

Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning a sat solver from single-bit supervision, 2019. [ bib | arXiv | .pdf ]

[8]

Daan Leijen, Benjamin Zorn, and Leonardo de Moura. Mimalloc: Free list sharding in action. In Anthony Widjaja Lin, editor, Programming Languages and Systems, pages 244--265, Cham, 2019. Springer International Publishing. [ bib | .pdf ]

[9]

Nikolaj Bjørner, Leonardo de Moura, Lev Nachmanson, and Christoph M. Wintersteiger. Programming Z3. In Engineering Trustworthy Software Systems - 4th International School, SETSS 2018, Chongqing, China, April 7-12, 2018, Tutorial Lectures, pages 148--201, 2018. [ bib | DOI | http ]

[10]

Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning a SAT solver from single-bit supervision. CoRR, abs/1802.03685, 2018. [ bib | arXiv | http ]

[11]

Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. A Metaprogramming Framework for Formal Verification. Proc. ACM Program. Lang., 1(ICFP):34:1--34:29, August 2017. [ bib | DOI | .pdf ]

Keywords: dependent type theory, metaprogramming, tactic language, theorem proving

[12]

Daniel Selsam and Leonardo de Moura. Congruence Closure in Intensional Type Theory. In Automated Reasoning, 8th International Joint Conference, University of Coimbra, Portugal, pages 99--115. Springer, 2016. [ bib | .pdf ]

[13]

Clark Barrett, Leonardo de Moura, and Pascal Fontaine. Proofs in Satisfiability Modulo Theories. Mathematical Logic and Foundations. College Publications, London, UK, 2015. [ bib | .pdf ]

[14]

Leonardo de Moura, Jeremy Avigad, Soonho Kong, and Cody Roux. Elaboration in dependent type theory, 2015. Preprint, http://arxiv.org/abs/1505.04324. [ bib | .pdf ]

[15]

Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover. In Automated Deduction - CADE-25, 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, 2015. [ bib | .pdf ]

[16]

Jeremy Avigad, Leonardo de Moura, and Soonho Kong. Theorem Proving in Lean. 2015. [ bib | .pdf ]

[17]

Andrew Reynolds, Cesare Tinelli, and Leonardo de Moura. Finding Conflicting Instances of Quantified Formulas in SMT. In Proceedings of 14th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2014, 21-24 October 2014, Lausanne, Switzerland, 2014. [ bib | .pdf ]

[18]

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 ]

[19]

Leonardo de Moura and Grant Passmore. The Strategy Challenge in SMT Solving, volume 7788 of Lecture Notes in Artificial Intelligence. Springer, 2013. [ bib | .pdf ]

[20]

Dejan Jovanović and Leonardo de Moura. Cutting to the chase: Solving linear integer arithmetic (to appear). Journal Automated Reasoning, 2013. [ bib | .pdf ]

[21]

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 ]

[22]

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 ]

[23]

Nikolaj Bjørner and Leonardo de Moura. Tractability and Modern Satisfiability Modulo Theories Solvers. In Handbook of Tractability. Cambridge University Press, 2012. [ bib | .pdf ]

[24]

Christoph Wintersteiger, Youssef Hamadi, and Leonardo de Moura. Efficiently solving quantified bit-vector formulas. Formal Methods in System Design, 2012. [ bib | http | .pdf ]

[25]

Clark Barrett, Morgan Deters, Leonardo de Moura, Albert Oliveras, and Aaron Stump. 6 Years of SMT-COMP. Journal of Automated Reasoning, 2012. [ bib | http ]

[26]

Dejan Jovanović and Leonardo de Moura. Solving non-linear arithmetic. Technical Report MSR-TR-2012-20, Microsoft Research, 2012. [ bib | http ]

[27]

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 ]

[28]

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 ]

[29]

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 ]

[30]

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 ]

[31]

Leonardo de Moura and Nikolaj Bjørner. Satisfiability modulo theories: introduction and applications. Commun. ACM, 54(9):69--77, 2011. [ bib | http ]

[32]

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 ]

[33]

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 ]

[34]

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 ]

[35]

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 ]

[36]

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 ]

[37]

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 ]

[38]

Leonardo de Moura and Grant Olney Passmore. On locally minimal nullstellensatz proofs. Technical Report MSR-TR-2009-90, Microsoft Research, 2009. [ bib | .pdf ]

[39]

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 ]

[40]

Nikolaj Bjørner and Leonardo de Moura. z3¹⁰: Applications, enablers, challenges and directions. In Sixth International Workshop on Constraints in Formal Verification Grenoble, France, 2009. [ bib | .pdf ]

[41]

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 ]

[42]

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 ]

[43]

Yeting Ge and Leonardo de Moura. Complete instantiation for quantified formulas in satisfiability modulo theories (extended version). 2009. [ bib | .pdf ]

[44]

Yeting Ge and Leonardo de Moura. Complete instantiation for quantified formulas in satisfiability 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 ]

[45]

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 ]

[46]

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 ]

[47]

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 ]

[48]

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 ]

[49]

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 ]

[50]

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 ]

[51]

Leonardo de Moura and Nikolaj Bjørner. Model-based theory combination. Electr. Notes Theor. Comput. Sci., 198(2):37--49, 2008. [ bib | .pdf ]

[52]

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 ]

[53]

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 ]

[54]

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 ]

[55]

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 ]

[56]

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 ]

[57]

Leonardo de Moura and Nikolaj Bjørner. Relevancy propagation. Technical Report MSR-TR-2007-140, Microsoft Research, 2007. [ bib | .pdf ]

[58]

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 ]

[59]

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 ]

[60]

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 ]

[61]

Bruno Dutertre and Leonardo de Moura. Integrating simplex with DPLL(T). Technical report, SRI International, 2006. [ bib | .pdf ]

[62]

Bruno Dutertre and Leonardo de Moura. The Yices SMT solver. Technical report, SRI International, 2006. [ bib | .pdf ]

[63]

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 ]

[64]

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 ]

[65]

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 ]

[66]

Grégoire Hamon, Leonardo de Moura, and John Rushby. Automated test generation with SAL. Technical report, SRI International, 2005. CSL Technical Note. [ bib | .pdf ]

[67]

Leonardo de Moura, Harald Rueß, and Natarajan Shankar. Justifying equality. Electr. Notes Theor. Comput. Sci., 125(3):69--85, 2005. [ bib | .pdf ]

[68]

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 ]

[69]

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 ]

[70]

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 ]

[71]

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 ]

[72]

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 ]

[73]

Leonardo de Moura, Harald Rueß, John Rushby, and Natarajan Shankar. Embedded deduction with ICS, 2003. [ bib | .pdf ]

[74]

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 ]

[75]

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 ]

[76]

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 ]

[77]

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 ]

[78]

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.99.