default search action
Leonardo Mendonça de Moura
Person information
- affiliation: Microsoft Research
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2022
- [j17]Sebastian Ullrich
, Leonardo de Moura:
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages. Log. Methods Comput. Sci. 18(2) (2022) - [j16]Sebastian Ullrich
'do' unchained: embracing local imperativity in a purely functional language (functional pearl). Proc. ACM Program. Lang. 6(ICFP): 512-539 (2022) - [e5]June Andronick, Leonardo de Moura
13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel. LIPIcs 237, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2022, ISBN 978-3-95977-252-5 [contents] - 2021
- [c57]Leonardo de Moura
The Lean 4 Theorem Prover and Programming Language. CADE 2021: 625-635 - [c56]Alex Reinking
Perceus: garbage free reference counting with reuse. PLDI 2021: 96-111 - 2020
- [j15]Leonardo de Moura
Preface: Selected Extended Papers of CADE 2017. J. Autom. Reason. 64(3): 511 (2020) - [j14]Daniel Selsam, Simon Hudon, Leonardo de Moura:
Sealing pointer-based optimizations behind pure functions. Proc. ACM Program. Lang. 4(ICFP): 115:1-115:20 (2020) - [c55]Sebastian Ullrich
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages. IJCAR (2) 2020: 167-182 - [i9]Daniel Selsam, Sebastian Ullrich, Leonardo de Moura:
Tabled Typeclass Resolution. CoRR abs/2001.04301 (2020) - [i8]Sebastian Ullrich
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages. CoRR abs/2001.10490 (2020) - [i7]Daniel Selsam, Simon Hudon, Leonardo de Moura:
Sealing Pointer-Based Optimizations Behind Pure Functions. CoRR abs/2003.01685 (2020) - [i6]Daniel Selsam, Jesse Michael Han, Leonardo de Moura, Patrice Godefroid:
Universal Policies for Software-Defined MDPs. CoRR abs/2012.11401 (2020)
2010 – 2019
- 2019
- [c54]Daan Leijen, Benjamin Zorn, Leonardo de Moura:
Mimalloc: Free List Sharding in Action. APLAS 2019: 244-265 - [c53]Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, David L. Dill:
Learning a SAT Solver from Single-Bit Supervision. ICLR (Poster) 2019 - [c52]Sebastian Ullrich, Leonardo de Moura:
Counting immutable beans: reference counting optimized for purely functional programming. IFL 2019: 3:1-3:12 - [i5]Sebastian Ullrich, Leonardo de Moura:
Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming. CoRR abs/1908.05647 (2019) - 2018
- [c51]Nikolaj S. Bjørner, Leonardo de Moura, Lev Nachmanson, Christoph M. Wintersteiger
Programming Z3. SETSS 2018: 148-201 - [i4]Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, David L. Dill:
Learning a SAT Solver from Single-Bit Supervision. CoRR abs/1802.03685 (2018) - 2017
- [j13]Gabriel Ebner, Sebastian Ullrich
A metaprogramming framework for formal verification. Proc. ACM Program. Lang. 1(ICFP): 34:1-34:29 (2017) - [e4]Leonardo de Moura:
Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings. Lecture Notes in Computer Science 10395, Springer 2017, ISBN 978-3-319-63045-8 [contents] - [i3]Daniel Selsam, Leonardo de Moura:
Congruence Closure in Intensional Type Theory. CoRR abs/1701.04391 (2017) - 2016
- [c50]Daniel Selsam, Leonardo de Moura:
Congruence Closure in Intensional Type Theory. IJCAR 2016: 99-115 - [c49]Leonardo Mendonça de Moura:
Dependent type practice (invited talk). CPP 2016: 2 - [c48]Leonardo de Moura:
Formalizing Mathematics using the Lean Theorem Prover. ISAIM 2016 - [e3]Michael Kohlhase, Moa Johansson, Bruce R. Miller, Leonardo de Moura, Frank Wm. Tompa
Intelligent Computer Mathematics - 9th International Conference, CICM 2016, Bialystok, Poland, July 25-29, 2016, Proceedings. Lecture Notes in Computer Science 9791, Springer 2016, ISBN 978-3-319-42546-7 [contents] - 2015
- [c47]Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad
The Lean Theorem Prover (System Description). CADE 2015: 378-388 - [e2]Stephan Schulz, Leonardo de Moura, Boris Konev:
4th Workshop on Practical Aspects of Automated Reasoning, PAAR@IJCAR 2014, Vienna, Austria, 2014. EPiC Series in Computing 31, EasyChair 2015 [contents] - [i2]Leonardo Mendonça de Moura, Jeremy Avigad, Soonho Kong, Cody Roux:
Elaboration in Dependent Type Theory. CoRR abs/1505.04324 (2015) - 2014
- [c46]Andrew Reynolds, Cesare Tinelli
Finding conflicting instances of quantified formulas in SMT. FMCAD 2014: 195-202 - [p1]Nikolaj S. Bjørner, Leonardo Mendonça de Moura:
Tractability and Modern Satisfiability Modulo Theories Solvers. Tractability 2014: 350-377 - 2013
- [j12]Christoph M. Wintersteiger
Efficiently solving quantified bit-vector formulas. Formal Methods Syst. Des. 42(1): 3-23 (2013) - [j11]Clark W. Barrett
6 Years of SMT-COMP. J. Autom. Reason. 50(3): 243-277 (2013) - [j10]Dejan Jovanovic, Leonardo Mendonça de Moura:
Cutting to the Chase - Solving Linear Integer Arithmetic. J. Autom. Reason. 51(1): 79-108 (2013) - [c45]Leonardo Mendonça de Moura, Grant Olney Passmore:
The Strategy Challenge in SMT Solving. Automated Reasoning and Mathematics 2013: 15-44 - [c44]Leonardo Mendonça de Moura, Grant Olney Passmore:
Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. CADE 2013: 178-192 - [c43]Leonardo Mendonça de Moura, Dejan Jovanovic:
Model-Driven Decision Procedures for Arithmetic. SYNASC 2013: 11 - [c42]Leonardo Mendonça de Moura, Dejan Jovanovic:
A Model-Constructing Satisfiability Calculus. VMCAI 2013: 1-12 - [e1]Juliano Iyoda, Leonardo Mendonça de Moura:
Formal Methods: Foundations and Applications - 16th Brazilian Symposium, SBMF 2013, Brasilia, Brazil, September 29 - October 4, 2013, Proceedings. Lecture Notes in Computer Science 8195, Springer 2013, ISBN 978-3-642-41070-3 [contents] - 2012
- [j9]Dejan Jovanovic, Leonardo de Moura:
Solving non-linear arithmetic. ACM Commun. Comput. Algebra 46(3/4): 104-105 (2012) - [c41]Grant Olney Passmore, Lawrence C. Paulson
Real Algebraic Strategies for MetiTarski Proofs. AISC/MKM/Calculemus 2012: 358-370 - [c40]Leonardo Mendonça de Moura:
Regression Tests and the Inventor's Dilemma. COMPARE 2012: 1 - [c39]Dejan Jovanovic, Leonardo Mendonça de Moura:
Solving Non-linear Arithmetic. IJCAR 2012: 339-354 - [c38]Thomas Ball, Nikolaj S. Bjørner, Leonardo Mendonça de Moura, Kenneth L. McMillan, Margus Veanes:
Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials. SPIN 2012: 1-6 - 2011
- [j8]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9): 69-77 (2011) - [j7]Maria Paola Bonacina
On Deciding Satisfiability by Theorem Proving with Speculative Inferences. J. Autom. Reason. 47(2): 161-189 (2011) - [c37]Dejan Jovanovic, Leonardo Mendonça de Moura:
Cutting to the Chase Solving Linear Integer Arithmetic. CADE 2011: 338-353 - [c36]Krystof Hoder, Nikolaj S. Bjørner, Leonardo Mendonça de Moura:
μZ- An Efficient Engine for Fixed Points with Constraints. CAV 2011: 457-462 - [c35]Leonardo Mendonça de Moura:
Orchestrating Satisfiability Engines. CP 2011: 1 - [c34]Leonardo Mendonça de Moura:
Satisfiability at Microsoft. FMICS 2011: 5 - 2010
- [j6]Ruzica Piskac
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. J. Autom. Reason. 44(4): 401-424 (2010) - [c33]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Applications and Challenges in Satisfiability Modulo Theories. WING@ETAPS/IJCAR 2010: 1-11 - [c32]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development. IJCAR 2010: 400-411 - [c31]Christoph M. Wintersteiger, Youssef Hamadi, Leonardo Mendonça de Moura:
Efficiently solving quantified bit-vector formulas. FMCAD 2010: 239-246 - [c30]Clark W. Barrett
The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk). Haifa Verification Conference 2010: 3 - [c29]Leonardo Mendonça de Moura, Carsten Lutz, Monica M. C. Schraefel, Bernhard Nebel:
Tutorial Presentations at the Twelfth International Conference on Principles of Knowledge Representation and Reasoning. KR 2010 - [c28]Margus Veanes, Nikolaj S. Bjørner, Leonardo Mendonça de Moura:
Symbolic Automata Constraint Solving. LPAR (Yogyakarta) 2010: 640-654 - [i1]Grant Olney Passmore, Leonardo Mendonça de Moura, Paul B. Jackson:
Gröbner Basis Construction Algorithms Based on Theorem Proving Saturation Loops. Decision Procedures in Software, Hardware and Bioware 2010
2000 – 2009
- 2009
- [c27]Maria Paola Bonacina
On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving. CADE 2009: 35-50 - [c26]Yeting Ge, Leonardo Mendonça de Moura:
Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. CAV 2009: 306-320 - [c25]Christoph M. Wintersteiger
A Concurrent Portfolio Approach to SMT Solving. CAV 2009: 715-720 - [c24]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Generalized, efficient array decision procedures. FMCAD 2009: 45-52 - [c23]Nikolaj S. Bjørner, Leonardo Mendonça de Moura:
Tapas: Theory Combinations and Practical Applications. FORMATS 2009: 1-6 - [c22]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Satisfiability Modulo Theories: An Appetizer. SBMF 2009: 23-36 - [c21]Grant Olney Passmore, Leonardo Mendonça de Moura:
Superfluous S-polynomials in Strategy-Independent Groebner Bases. SYNASC 2009: 45-53 - 2008
- [c20]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. IJCAR 2008: 410-425 - [c19]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Engineering DPLL(T) + Saturation. IJCAR 2008: 475-490 - [c18]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Proofs and Refutations, and Z3. LPAR Workshops 2008 - [c17]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Z3: An Efficient SMT Solver. TACAS 2008: 337-340 - 2007
- [j5]Clark W. Barrett
Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006). Formal Methods Syst. Des. 31(3): 221-239 (2007) - [c16]Leonardo Mendonça de Moura:
Invited talk: Developing Efficient SMT Solvers. ESARLT 2007 - [c15]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Efficient E-Matching for SMT Solvers. CADE 2007: 183-198 - [c14]Leonardo Mendonça de Moura, Bruno Dutertre, Natarajan Shankar:
A Tutorial on Satisfiability Modulo Theories. CAV 2007: 20-36 - [c13]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Model-based Theory Combination. SMT@CAV 2007: 37-49 - 2006
- [c12]Bruno Dutertre, Leonardo Mendonça de Moura:
A Fast Linear-Arithmetic Solver for DPLL(T). CAV 2006: 81-94 - 2005
- [j4]Clark W. Barrett
Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005). J. Autom. Reason. 35(4): 373-390 (2005) - [c11]Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump:
SMT-COMP: Satisfiability Modulo Theories Competition. CAV 2005: 20-23 - 2004
- [c10]Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar:
The ICS Decision Procedures for Embedded Deduction. IJCAR 2004: 218-222 - [c9]Leonardo Mendonça de Moura, Harald Rueß:
An Experimental Evaluation of Ground Decision Procedures. CAV 2004: 162-174 - [c8]Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar, Maria Sorea, Ashish Tiwari:
SAL 2. CAV 2004: 496-500 - [c7]Grégoire Hamon, Leonardo Mendonça de Moura, John M. Rushby:
Generating Efficient Test Sets with a Model Checker. SEFM 2004: 261-270 - [c6]Leonardo Mendonça de Moura, Harald Rueß, Natarajan Shankar:
Justifying Equality. D/PDPAR@IJCAR 2004: 69-85 - 2003
- [c5]Leonardo Mendonça de Moura, Harald Rueß, Maria Sorea:
Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A). CAV 2003: 14-26 - [c4]Harald Rueß, Leonardo Mendonça de Moura:
Simulation and verification I: from simulation to verification (and back). WSC 2003: 888-896 - 2002
- [c3]Leonardo Mendonça de Moura, Harald Rueß, Maria Sorea:
Lazy Theorem Proving for Bounded Model Checking over Infinite Domains. CADE 2002: 438-455 - 2000
- [j3]Marcus Fontoura, Christiano Braga, Leonardo Mendonça de Moura, Carlos Lucena:
Using domain specific languages to instantiate object-oriented frameworks. IEE Proc. Softw. 147(4): 109-116 (2000)
1990 – 1999
- 1999
- [j2]Leonardo Mendonça de Moura, Carlos José Pereira de Lucena, Arndt von Staa:
The Spider Environment. Softw. Pract. Exp. 29(2): 99-124 (1999) - 1998
- [c2]Ira D. Baxter, Andrew Yahin, Leonardo Mendonça de Moura, Marcelo Sant'Anna, Lorraine Bier:
Clone Detection Using Abstract Syntax Trees. ICSM 1998: 368-377 - 1997
- [j1]Leonardo Mendonça de Moura, Carlos José Pereira de Lucena:
O Ambiente Visual Spider para o Desenvolvimento de Aplicações para a Internet. RITA 4(2): 59-78 (1997) - [c1]Leonardo Mendonça de Moura, Carlos José Pereira de Lucena:
Introdução ao Ambiente Visual Spider. SBES 1997: 3-13
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-22 19:48 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: