Leonardo Mendonça de Moura

Orcid: 0000-0002-5158-4726

Affiliations:
  • Microsoft Research


According to our database1, Leonardo Mendonça de Moura authored at least 75 papers between 1997 and 2022.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2022
'do' unchained: embracing local imperativity in a purely functional language (functional pearl).
Proc. ACM Program. Lang., 2022

Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages.
Log. Methods Comput. Sci., 2022

2021
Perceus: garbage free reference counting with reuse.
Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

The Lean 4 Theorem Prover and Programming Language.
Proceedings of the Automated Deduction - CADE 28, 2021

2020
Sealing pointer-based optimizations behind pure functions.
Proc. ACM Program. Lang., 2020

Preface: Selected Extended Papers of CADE 2017.
J. Autom. Reason., 2020

Universal Policies for Software-Defined MDPs.
CoRR, 2020

Tabled Typeclass Resolution.
CoRR, 2020

2019
Counting immutable beans: reference counting optimized for purely functional programming.
Proceedings of the IFL '19: Implementation and Application of Functional Languages, 2019

Learning a SAT Solver from Single-Bit Supervision.
Proceedings of the 7th International Conference on Learning Representations, 2019

Mimalloc: Free List Sharding in Action.
Proceedings of the Programming Languages and Systems - 17th Asian Symposium, 2019

2018
Programming Z3.
Proceedings of the Engineering Trustworthy Software Systems - 4th International School, 2018

2017
A metaprogramming framework for formal verification.
Proc. ACM Program. Lang., 2017

2016
Formalizing Mathematics using the Lean Theorem Prover.
Proceedings of the International Symposium on Artificial Intelligence and Mathematics, 2016

Dependent type practice (invited talk).
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

Congruence Closure in Intensional Type Theory.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015
Elaboration in Dependent Type Theory.
CoRR, 2015

The Lean Theorem Prover (System Description).
Proceedings of the Automated Deduction - CADE-25, 2015

2014
Finding conflicting instances of quantified formulas in SMT.
Proceedings of the Formal Methods in Computer-Aided Design, 2014

Tractability and Modern Satisfiability Modulo Theories Solvers.
Proceedings of the Tractability: Practical Approaches to Hard Problems, 2014

2013
Cutting to the Chase - Solving Linear Integer Arithmetic.
J. Autom. Reason., 2013

6 Years of SMT-COMP.
J. Autom. Reason., 2013

Efficiently solving quantified bit-vector formulas.
Formal Methods Syst. Des., 2013

A Model-Constructing Satisfiability Calculus.
Proceedings of the Verification, 2013

Model-Driven Decision Procedures for Arithmetic.
Proceedings of the 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2013

Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals.
Proceedings of the Automated Deduction - CADE-24, 2013

The Strategy Challenge in SMT Solving.
Proceedings of the Automated Reasoning and Mathematics, 2013

2012
Solving non-linear arithmetic.
ACM Commun. Comput. Algebra, 2012

Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials.
Proceedings of the Model Checking Software - 19th International Workshop, 2012

Regression Tests and the Inventor's Dilemma.
Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, 2012

Real Algebraic Strategies for MetiTarski Proofs.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

2011
On Deciding Satisfiability by Theorem Proving with Speculative Inferences.
J. Autom. Reason., 2011

Satisfiability modulo theories: introduction and applications.
Commun. ACM, 2011

Satisfiability at Microsoft.
Proceedings of the Formal Methods for Industrial Critical Systems, 2011

Orchestrating Satisfiability Engines.
Proceedings of the Principles and Practice of Constraint Programming - CP 2011, 2011

<i>μZ</i>- An Efficient Engine for Fixed Points with Constraints.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets.
J. Autom. Reason., 2010

Symbolic Automata Constraint Solving.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Tutorial Presentations at the Twelfth International Conference on Principles of Knowledge Representation and Reasoning.
Proceedings of the Principles of Knowledge Representation and Reasoning: Proceedings of the Twelfth International Conference, 2010

The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk).
Proceedings of the Hardware and Software: Verification and Testing, 2010

Gröbner Basis Construction Algorithms Based on Theorem Proving Saturation Loops.
Proceedings of the Decision Procedures in Software, Hardware and Bioware, 18.04., 2010

Applications and Challenges in Satisfiability Modulo Theories.
Proceedings of the Second International Workshop on Invariant Generation, 2010

Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009
Superfluous S-polynomials in Strategy-Independent Groebner Bases.
Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2009

Satisfiability Modulo Theories: An Appetizer.
Proceedings of the Formal Methods: Foundations and Applications, 2009

Tapas: Theory Combinations and Practical Applications.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2009

Generalized, efficient array decision procedures.
Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

A Concurrent Portfolio Approach to SMT Solving.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

On Deciding Satisfiability by DPLL(G+<i>T</i>) and Unsound Theorem Proving.
Proceedings of the Automated Deduction, 2009

2008
Z3: An Efficient SMT Solver.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Proofs and Refutations, and Z3.
Proceedings of the LPAR 2008 Workshops, 2008

Engineering DPLL(T) + Saturation.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

Deciding Effectively Propositional Logic Using DPLL and Substitution Sets.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007
Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006).
Formal Methods Syst. Des., 2007

Model-based Theory Combination.
Proceedings of the 5th International Workshop on Satisfiability Modulo Theories, 2007

A Tutorial on Satisfiability Modulo Theories.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Efficient E-Matching for SMT Solvers.
Proceedings of the Automated Deduction, 2007

Invited talk: Developing Efficient SMT Solvers.
Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, 2007

2006
A Fast Linear-Arithmetic Solver for DPLL(T).
Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005
Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005).
J. Autom. Reason., 2005

SMT-COMP: Satisfiability Modulo Theories Competition.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004
Justifying Equality.
Proceedings of the Selected Papers from the Workshops on Disproving, 2004

Generating Efficient Test Sets with a Model Checker.
Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 2004

An Experimental Evaluation of Ground Decision Procedures.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

SAL 2.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

The ICS Decision Procedures for Embedded Deduction.
Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003
Simulation and verification I: from simulation to verification (and back).
Proceedings of the 35th Winter Simulation Conference: Driving Innovation, 2003

Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A).
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002
Lazy Theorem Proving for Bounded Model Checking over Infinite Domains.
Proceedings of the Automated Deduction, 2002

2000
Using domain specific languages to instantiate object-oriented frameworks.
IEE Proc. Softw., 2000

1999
The Spider Environment.
Softw. Pract. Exp., 1999

1998
Clone Detection Using Abstract Syntax Trees.
Proceedings of the 1998 International Conference on Software Maintenance, 1998

1997
O Ambiente Visual Spider para o Desenvolvimento de Aplicações para a Internet.
RITA, 1997

Introdução ao Ambiente Visual Spider.
Proceedings of the 11th Brazilian Symposium on Software Engineering, 1997


  Loading...