Leonardo Mendonça de Moura

62 papers A* 9A 13B 6C 1Misc 3Journal 12Unranked 16

Year	Rank	Type	Title / Venue / Authors
2016	B	`conf`	Dependent type practice (invited talk). CPP Leonardo Mendonça de Moura
2015	J	`jnl`	Elaboration in Dependent Type Theory. CoRR Leonardo Mendonça de Moura, Jeremy Avigad, Soonho Kong, Cody Roux
2015	A	`conf`	The Lean Theorem Prover (System Description). CADE Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer
2014	B	`conf`	Finding conflicting instances of quantified formulas in SMT. FMCAD Andrew Reynolds, Cesare Tinelli, Leonardo Mendonça de Moura
2014	—	`ch.`	Tractability and Modern Satisfiability Modulo Theories Solvers. Tractability Nikolaj S. Bjørner, Leonardo Mendonça de Moura
2013	J	`jnl`	6 Years of SMT-COMP. J. Autom. Reason. Clark W. Barrett, Morgan Deters, Leonardo Mendonça de Moura, Albert Oliveras, Aaron Stump
2013	B	`conf`	A Model-Constructing Satisfiability Calculus. VMCAI Leonardo Mendonça de Moura, Dejan Jovanovic
2013	A	`conf`	Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. CADE Leonardo Mendonça de Moura, Grant Olney Passmore
2013	J	`jnl`	Cutting to the Chase - Solving Linear Integer Arithmetic. J. Autom. Reason. Dejan Jovanovic, Leonardo Mendonça de Moura
2013	J	`jnl`	Efficiently solving quantified bit-vector formulas. Formal Methods Syst. Des. Christoph M. Wintersteiger, Youssef Hamadi, Leonardo Mendonça de Moura
2013	—	`ed.`	Formal Methods: Foundations and Applications - 16th Brazilian Symposium, SBMF 2013, Brasilia, Brazil, September 29 - October 4, 2013, Proceedings SBMF Juliano Iyoda, Leonardo Mendonça de Moura
2013	Misc	`conf`	Model-Driven Decision Procedures for Arithmetic. SYNASC Leonardo Mendonça de Moura, Dejan Jovanovic
2013	—	`conf`	The Strategy Challenge in SMT Solving. Automated Reasoning and Mathematics Leonardo Mendonça de Moura, Grant Olney Passmore
2012	—	`conf`	Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials. SPIN Thomas Ball, Nikolaj S. Bjørner, Leonardo Mendonça de Moura, Kenneth L. McMillan, Margus Veanes
2012	—	`conf`	Real Algebraic Strategies for MetiTarski Proofs. AISC/MKM/Calculemus Grant Olney Passmore, Lawrence C. Paulson, Leonardo Mendonça de Moura
2012	—	`conf`	Regression Tests and the Inventor's Dilemma. COMPARE Leonardo Mendonça de Moura
2012	A	`conf`	Solving Non-linear Arithmetic. IJCAR Dejan Jovanovic, Leonardo Mendonça de Moura
2011	A	`conf`	Cutting to the Chase Solving Linear Integer Arithmetic. CADE Dejan Jovanovic, Leonardo Mendonça de Moura
2011	J	`jnl`	On Deciding Satisfiability by Theorem Proving with Speculative Inferences. J. Autom. Reason. Maria Paola Bonacina, Christopher Lynch, Leonardo Mendonça de Moura
2011	A	`conf`	Orchestrating Satisfiability Engines. CP Leonardo Mendonça de Moura
2011	C	`conf`	Satisfiability at Microsoft. FMICS Leonardo Mendonça de Moura
2011	J	`jnl`	Satisfiability modulo theories: introduction and applications. Commun. ACM Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2010	—	`conf`	Applications and Challenges in Satisfiability Modulo Theories. WING@ETAPS/IJCAR Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2010	A	`conf`	Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development. IJCAR Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2010	J	`jnl`	Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. J. Autom. Reason. Ruzica Piskac, Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2010	B	`conf`	Efficiently solving quantified bit-vector formulas. FMCAD Christoph M. Wintersteiger, Youssef Hamadi, Leonardo Mendonça de Moura
2010	—	`conf`	Gröbner Basis Construction Algorithms Based on Theorem Proving Saturation Loops. Decision Procedures in Software, Hardware and Bioware Grant Olney Passmore, Leonardo Mendonça de Moura, Paul B. Jackson
2010	—	`conf`	Symbolic Automata Constraint Solving. LPAR (Yogyakarta) Margus Veanes, Nikolaj S. Bjørner, Leonardo Mendonça de Moura
2010	—	`conf`	The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk). Haifa Verification Conference Clark W. Barrett, Leonardo Mendonça de Moura, Silvio Ranise, Aaron Stump, Cesare Tinelli
2010	A*	`conf`	Tutorial Presentations at the Twelfth International Conference on Principles of Knowledge Representation and Reasoning. KR Leonardo Mendonça de Moura, Carsten Lutz, Monica M. C. Schraefel, Bernhard Nebel
2009	A*	`conf`	A Concurrent Portfolio Approach to SMT Solving. CAV Christoph M. Wintersteiger, Youssef Hamadi, Leonardo Mendonça de Moura
2009	A*	`conf`	Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. CAV Yeting Ge, Leonardo Mendonça de Moura
2009	B	`conf`	Generalized, efficient array decision procedures. FMCAD Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2009	A	`conf`	On Deciding Satisfiability by DPLL(G+ CADE Maria Paola Bonacina, Christopher Lynch, Leonardo Mendonça de Moura
2009	—	`conf`	Satisfiability Modulo Theories: An Appetizer. SBMF Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2009	Misc	`conf`	Superfluous S-polynomials in Strategy-Independent Groebner Bases. SYNASC Grant Olney Passmore, Leonardo Mendonça de Moura
2009	—	`conf`	Tapas: Theory Combinations and Practical Applications. FORMATS Nikolaj S. Bjørner, Leonardo Mendonça de Moura
2008	A	`conf`	Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. IJCAR Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2008	A	`conf`	Engineering DPLL(T) + Saturation. IJCAR Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2008	—	`conf`	Proofs and Refutations, and Z3. LPAR Workshops Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2008	A	`conf`	Z3: An Efficient SMT Solver. TACAS Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2007	A*	`conf`	A Tutorial on Satisfiability Modulo Theories. CAV Leonardo Mendonça de Moura, Bruno Dutertre, Natarajan Shankar
2007	J	`jnl`	Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006). Formal Methods Syst. Des. Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump
2007	A	`conf`	Efficient E-Matching for SMT Solvers. CADE Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2007	—	`conf`	Invited talk: Developing Efficient SMT Solvers. ESARLT Leonardo Mendonça de Moura
2007	—	`conf`	Model-based Theory Combination. SMT@CAV Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2006	A*	`conf`	A Fast Linear-Arithmetic Solver for DPLL(T). CAV Bruno Dutertre, Leonardo Mendonça de Moura
2005	J	`jnl`	Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005). J. Autom. Reason. Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump
2005	A*	`conf`	SMT-COMP: Satisfiability Modulo Theories Competition. CAV Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump
2004	A*	`conf`	An Experimental Evaluation of Ground Decision Procedures. CAV Leonardo Mendonça de Moura, Harald Rueß
2004	B	`conf`	Generating Efficient Test Sets with a Model Checker. SEFM Grégoire Hamon, Leonardo Mendonça de Moura, John M. Rushby
2004	—	`conf`	Justifying Equality. D/PDPAR@IJCAR Leonardo Mendonça de Moura, Harald Rueß, Natarajan Shankar
2004	A*	`conf`	SAL 2. CAV Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar, Maria Sorea, Ashish Tiwari
2004	A	`conf`	The ICS Decision Procedures for Embedded Deduction. IJCAR Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar
2003	A*	`conf`	Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A). CAV Leonardo Mendonça de Moura, Harald Rueß, Maria Sorea
2003	Misc	`conf`	Simulation and verification I: from simulation to verification (and back). WSC Harald Rueß, Leonardo Mendonça de Moura
2002	A	`conf`	Lazy Theorem Proving for Bounded Model Checking over Infinite Domains. CADE Leonardo Mendonça de Moura, Harald Rueß, Maria Sorea
2000	J	`jnl`	Using domain specific languages to instantiate object-oriented frameworks. IEE Proc. Softw. Marcus Fontoura, Christiano Braga, Leonardo Mendonça de Moura, Carlos Lucena
1999	J	`jnl`	The Spider Environment. Softw. Pract. Exp. Leonardo Mendonça de Moura, Carlos José Pereira de Lucena, Arndt von Staa
1998	—	`conf`	Clone Detection Using Abstract Syntax Trees. ICSM Ira D. Baxter, Andrew Yahin, Leonardo Mendonça de Moura, Marcelo Sant'Anna, Lorraine Bier
1997	—	`conf`	Introdução ao Ambiente Visual Spider. SBES Leonardo Mendonça de Moura, Carlos José Pereira de Lucena
1997	J	`jnl`	O Ambiente Visual Spider para o Desenvolvimento de Aplicações para a Internet. RITA Leonardo Mendonça de Moura, Carlos José Pereira de Lucena