Leonardo Mendona de Moura
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
39
Venues
14
Active years
2002–2016
Best venue rank
A*
Where they publish
Papers
39 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2016 | CPP | Dependent type practice (invited talk). | Leonardo Mendona de Moura |
| 2015 | CADE | The Lean Theorem Prover (System Description). | Leonardo Mendona de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer |
| 2014 | FMCAD | Finding conflicting instances of quantified formulas in SMT. | Andrew Reynolds, Cesare Tinelli, Leonardo Mendona de Moura |
| 2013 | CADE | Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. | Leonardo Mendona de Moura, Grant Olney Passmore |
| 2013 | SYNASC | Model-Driven Decision Procedures for Arithmetic. | Leonardo Mendona de Moura, Dejan Jovanovic |
| 2013 | VMCAI | A Model-Constructing Satisfiability Calculus. | Leonardo Mendona de Moura, Dejan Jovanovic |
| 2012 | AISC | Real Algebraic Strategies for MetiTarski Proofs. | Grant Olney Passmore, Lawrence C. Paulson, Leonardo Mendona de Moura |
| 2012 | CADE | Solving Non-linear Arithmetic. | Dejan Jovanovic, Leonardo Mendona de Moura |
| 2012 | CADE | Regression Tests and the Inventor's Dilemma. | Leonardo Mendona de Moura |
| 2011 | CADE | Cutting to the Chase Solving Linear Integer Arithmetic. | Dejan Jovanovic, Leonardo Mendona de Moura |
| 2011 | CAV | Untitled record | Krystof Hoder, Nikolaj S. Bjrner, Leonardo Mendona de Moura |
| 2011 | CP | Orchestrating Satisfiability Engines. | Leonardo Mendona de Moura |
| 2011 | FMICS | Satisfiability at Microsoft. | Leonardo Mendona de Moura |
| 2010 | CADE | Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2010 | CADE | Applications and Challenges in Satisfiability Modulo Theories. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2010 | FMCAD | Efficiently solving quantified bit-vector formulas. | Christoph M. Wintersteiger, Youssef Hamadi, Leonardo Mendona de Moura |
| 2010 | KR | Tutorial Presentations at the Twelfth International Conference on Principles of Knowledge Representation and Reasoning. | Leonardo Mendona de Moura, Carsten Lutz, Monica M. C. Schraefel, Bernhard Nebel |
| 2010 | LPAR | Symbolic Automata Constraint Solving. | Margus Veanes, Nikolaj S. Bjrner, Leonardo Mendona de Moura |
| 2009 | CADE | On Deciding Satisfiability by DPLL(G+ | Maria Paola Bonacina, Christopher Lynch, Leonardo Mendona de Moura |
| 2009 | CAV | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. | Yeting Ge, Leonardo Mendona de Moura |
| 2009 | CAV | A Concurrent Portfolio Approach to SMT Solving. | Christoph M. Wintersteiger, Youssef Hamadi, Leonardo Mendona de Moura |
| 2009 | FMCAD | Generalized, efficient array decision procedures. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2009 | SYNASC | Superfluous S-polynomials in Strategy-Independent Groebner Bases. | Grant Olney Passmore, Leonardo Mendona de Moura |
| 2008 | CADE | Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2008 | CADE | Engineering DPLL(T) + Saturation. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2008 | LPAR | Proofs and Refutations, and Z3. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2008 | TACAS | Z3: An Efficient SMT Solver. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2007 | CADE | Invited talk: Developing Efficient SMT Solvers. | Leonardo Mendona de Moura |
| 2007 | CADE | Efficient E-Matching for SMT Solvers. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2007 | CAV | A Tutorial on Satisfiability Modulo Theories. | Leonardo Mendona de Moura, Bruno Dutertre, Natarajan Shankar |
| 2006 | CAV | A Fast Linear-Arithmetic Solver for DPLL(T). | Bruno Dutertre, Leonardo Mendona de Moura |
| 2005 | CAV | SMT-COMP: Satisfiability Modulo Theories Competition. | Clark W. Barrett, Leonardo Mendona de Moura, Aaron Stump |
| 2004 | CADE | The ICS Decision Procedures for Embedded Deduction. | Leonardo Mendona de Moura, Sam Owre, Harald Rue, John M. Rushby, Natarajan Shankar |
| 2004 | CAV | SAL 2. | Leonardo Mendona de Moura, Sam Owre, Harald Rue, John M. Rushby, Natarajan Shankar, Maria Sorea, Ashish Tiwari |
| 2004 | CAV | An Experimental Evaluation of Ground Decision Procedures. | Leonardo Mendona de Moura, Harald Rue |
| 2004 | SEFM | Generating Efficient Test Sets with a Model Checker. | Grgoire Hamon, Leonardo Mendona de Moura, John M. Rushby |
| 2003 | CAV | Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A). | Leonardo Mendona de Moura, Harald Rue, Maria Sorea |
| 2003 | WSC | Simulation and verification I: from simulation to verification (and back). | Harald Rue, Leonardo Mendona de Moura |
| 2002 | CADE | Lazy Theorem Proving for Bounded Model Checking over Infinite Domains. | Leonardo Mendona de Moura, Harald Rue, Maria Sorea |