Introdução ao Ambiente Visual Spider. - Leonardo Mendonça de Moura; Carlos José Pereira de Lucena (SBES, 1997)

O Ambiente Visual Spider para o Desenvolvimento de Aplicações para a Internet. - Leonardo Mendonça de Moura; Carlos José Pereira de Lucena (RITA, 1997)

Clone Detection Using Abstract Syntax Trees. - Ira D. Baxter; Andrew Yahin; Leonardo Mendonça de Moura; Marcelo Sant'Anna; Lorraine Bier (ICSM, 1998)

The Spider Environment. - Leonardo Mendonça de Moura; Carlos José Pereira de Lucena; Arndt von Staa (Softw. Pract. Exp., 1999)

Using domain specific languages to instantiate object-oriented frameworks. - Marcus Fontoura; Christiano Braga; Leonardo Mendonça de Moura; Carlos Lucena (IEE Proc. Softw., 2000)

Lazy Theorem Proving for Bounded Model Checking over Infinite Domains. - Leonardo Mendonça de Moura; Harald Rueß; Maria Sorea (CADE, 2002)

Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A). - Leonardo Mendonça de Moura; Harald Rueß; Maria Sorea (CAV, 2003)

Simulation and verification I: from simulation to verification (and back). - Harald Rueß; Leonardo Mendonça de Moura (WSC, 2003)

The ICS Decision Procedures for Embedded Deduction. - Leonardo Mendonça de Moura; Sam Owre; Harald Rueß; John M. Rushby; Natarajan Shankar (IJCAR, 2004)

SAL 2. - Leonardo Mendonça de Moura; Sam Owre; Harald Rueß; John M. Rushby; Natarajan Shankar; Maria Sorea; Ashish Tiwari 001 (CAV, 2004)

An Experimental Evaluation of Ground Decision Procedures. - Leonardo Mendonça de Moura; Harald Rueß (CAV, 2004)

Generating Efficient Test Sets with a Model Checker. - Grégoire Hamon; Leonardo Mendonça de Moura; John M. Rushby (SEFM, 2004)

Justifying Equality. - Leonardo Mendonça de Moura; Harald Rueß; Natarajan Shankar (D/PDPAR@IJCAR, 2004)

SMT-COMP: Satisfiability Modulo Theories Competition. - Clark W. Barrett; Leonardo Mendonça de Moura; Aaron Stump (CAV, 2005)

Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005). - Clark W. Barrett; Leonardo Mendonça de Moura; Aaron Stump (J. Autom. Reason., 2005)

A Fast Linear-Arithmetic Solver for DPLL(T). - Bruno Dutertre; Leonardo Mendonça de Moura (CAV, 2006)

Invited talk: Developing Efficient SMT Solvers. - Leonardo Mendonça de Moura (ESARLT, 2007)

Efficient E-Matching for SMT Solvers. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (CADE, 2007)

A Tutorial on Satisfiability Modulo Theories. - Leonardo Mendonça de Moura; Bruno Dutertre; Natarajan Shankar (CAV, 2007)

Model-based Theory Combination. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (SMT@CAV, 2007)

Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006). - Clark W. Barrett; Leonardo Mendonça de Moura; Aaron Stump (Formal Methods Syst. Des., 2007)

Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (IJCAR, 2008)

Engineering DPLL(T) + Saturation. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (IJCAR, 2008)

Proofs and Refutations, and Z3. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (LPAR Workshops, 2008)

Z3: An Efficient SMT Solver. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (TACAS, 2008)

On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving. - Maria Paola Bonacina; Christopher Lynch; Leonardo Mendonça de Moura (CADE, 2009)

Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. - Yeting Ge; Leonardo Mendonça de Moura (CAV, 2009)

A Concurrent Portfolio Approach to SMT Solving. - Christoph M. Wintersteiger; Youssef Hamadi; Leonardo Mendonça de Moura (CAV, 2009)

Generalized, efficient array decision procedures. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (FMCAD, 2009)

Tapas: Theory Combinations and Practical Applications. - Nikolaj S. Bjørner; Leonardo Mendonça de Moura (FORMATS, 2009)

Satisfiability Modulo Theories: An Appetizer. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (SBMF, 2009)

Superfluous S-polynomials in Strategy-Independent Groebner Bases. - Grant Olney Passmore; Leonardo Mendonça de Moura (SYNASC, 2009)

Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (IJCAR, 2010)

Applications and Challenges in Satisfiability Modulo Theories. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (WING@ETAPS/IJCAR, 2010)

Gröbner Basis Construction Algorithms Based on Theorem Proving Saturation Loops. - Grant Olney Passmore; Leonardo Mendonça de Moura; Paul B. Jackson (Decision Procedures in Software, Hardware and Bioware, 2010)

Efficiently solving quantified bit-vector formulas. - Christoph M. Wintersteiger; Youssef Hamadi; Leonardo Mendonça de Moura (FMCAD, 2010)

The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk). - Clark W. Barrett; Leonardo Mendonça de Moura; Silvio Ranise; Aaron Stump; Cesare Tinelli (Haifa Verification Conference, 2010)

Tutorial Presentations at the Twelfth International Conference on Principles of Knowledge Representation and Reasoning. - Leonardo Mendonça de Moura; Carsten Lutz; Monica M. C. Schraefel; Bernhard Nebel (KR, 2010)

Symbolic Automata Constraint Solving. - Margus Veanes; Nikolaj S. Bjørner; Leonardo Mendonça de Moura (LPAR (Yogyakarta), 2010)

Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. - Ruzica Piskac; Leonardo Mendonça de Moura; Nikolaj S. Bjørner (J. Autom. Reason., 2010)

Cutting to the Chase Solving Linear Integer Arithmetic. - Dejan Jovanovic; Leonardo Mendonça de Moura (CADE, 2011)

μZ- An Efficient Engine for Fixed Points with Constraints. - Krystof Hoder; Nikolaj S. Bjørner; Leonardo Mendonça de Moura (CAV, 2011)

Orchestrating Satisfiability Engines. - Leonardo Mendonça de Moura (CP, 2011)

Satisfiability at Microsoft. - Leonardo Mendonça de Moura (FMICS, 2011)

Satisfiability modulo theories: introduction and applications. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (Commun. ACM, 2011)

On Deciding Satisfiability by Theorem Proving with Speculative Inferences. - Maria Paola Bonacina; Christopher Lynch; Leonardo Mendonça de Moura (J. Autom. Reason., 2011)

Real Algebraic Strategies for MetiTarski Proofs. - Grant Olney Passmore; Lawrence C. Paulson; Leonardo Mendonça de Moura (AISC/MKM/Calculemus, 2012)

Solving Non-linear Arithmetic. - Dejan Jovanovic; Leonardo Mendonça de Moura (IJCAR, 2012)

Regression Tests and the Inventor's Dilemma. - Leonardo Mendonça de Moura (COMPARE, 2012)

Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials. - Thomas Ball 001; Nikolaj S. Bjørner; Leonardo Mendonça de Moura; Kenneth L. McMillan; Margus Veanes (SPIN, 2012)

The Strategy Challenge in SMT Solving. - Leonardo Mendonça de Moura; Grant Olney Passmore (Automated Reasoning and Mathematics, 2013)

Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. - Leonardo Mendonça de Moura; Grant Olney Passmore (CADE, 2013)

Model-Driven Decision Procedures for Arithmetic. - Leonardo Mendonça de Moura; Dejan Jovanovic (SYNASC, 2013)

A Model-Constructing Satisfiability Calculus. - Leonardo Mendonça de Moura; Dejan Jovanovic (VMCAI, 2013)

6 Years of SMT-COMP. - Clark W. Barrett; Morgan Deters; Leonardo Mendonça de Moura; Albert Oliveras; Aaron Stump (J. Autom. Reason., 2013)

Tractability and Modern Satisfiability Modulo Theories Solvers. - Nikolaj S. Bjørner; Leonardo Mendonça de Moura (Tractability, 2014)

Finding conflicting instances of quantified formulas in SMT. - Andrew Reynolds 001; Cesare Tinelli; Leonardo Mendonça de Moura (FMCAD, 2014)

The Lean Theorem Prover (System Description). - Leonardo Mendonça de Moura; Soonho Kong; Jeremy Avigad; Floris van Doorn; Jakob von Raumer (CADE, 2015)

Elaboration in Dependent Type Theory. - Leonardo Mendonça de Moura; Jeremy Avigad; Soonho Kong; Cody Roux (CoRR, 2015)

Congruence Closure in Intensional Type Theory. - Daniel Selsam; Leonardo de Moura 001 (IJCAR, 2016)

Dependent type practice (invited talk). - Leonardo Mendonça de Moura (CPP, 2016)

Formalizing Mathematics using the Lean Theorem Prover. - Leonardo de Moura 001 (ISAIM, 2016)

A metaprogramming framework for formal verification. - Gabriel Ebner; Sebastian Ullrich 002; Jared Roesch; Jeremy Avigad; Leonardo de Moura 001 (Proc. ACM Program. Lang., 2017)

Programming Z3. - Nikolaj S. Bjørner; Leonardo de Moura 001; Lev Nachmanson; Christoph M. Wintersteiger (SETSS, 2018)

Mimalloc: Free List Sharding in Action. - Daan Leijen; Benjamin Zorn 001; Leonardo de Moura 001 (APLAS, 2019)

Learning a SAT Solver from Single-Bit Supervision. - Daniel Selsam; Matthew Lamm; Benedikt Bünz; Percy Liang; Leonardo de Moura 001; David L. Dill (ICLR (Poster), 2019)

Counting immutable beans: reference counting optimized for purely functional programming. - Sebastian Ullrich 002; Leonardo de Moura 001 (IFL, 2019)

Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages. - Sebastian Ullrich 002; Leonardo de Moura 001 (IJCAR (2), 2020)

Tabled Typeclass Resolution. - Daniel Selsam; Sebastian Ullrich 002; Leonardo de Moura 001 (CoRR, 2020)

Universal Policies for Software-Defined MDPs. - Daniel Selsam; Jesse Michael Han; Leonardo de Moura 001; Patrice Godefroid (CoRR, 2020)

Preface: Selected Extended Papers of CADE 2017. - Leonardo de Moura 001 (J. Autom. Reason., 2020)

Sealing pointer-based optimizations behind pure functions. - Daniel Selsam; Simon Hudon; Leonardo de Moura 001 (Proc. ACM Program. Lang., 2020)

The Lean 4 Theorem Prover and Programming Language. - Leonardo de Moura 001; Sebastian Ullrich 002 (CADE, 2021)

Perceus: garbage free reference counting with reuse. - Alex Reinking; Ningning Xie; Leonardo de Moura 001; Daan Leijen (PLDI, 2021)

'do' unchained: embracing local imperativity in a purely functional language (functional pearl). - Sebastian Ullrich 002; Leonardo de Moura 001 (Proc. ACM Program. Lang., 2022)

CSLib: The Lean Computer Science Library. - Clark W. Barrett; Swarat Chaudhuri; Fabrizio Montesi; Jim Grundy; Pushmeet Kohli; Leonardo de Moura 001; Alexandre Rademaker; Sorrachai Yingchareonthawornchai (CoRR, 2026)