Travelled to:1 × Australia
1 × Canada
1 × China
1 × Denmark
1 × France
1 × Hungary
1 × Ireland
1 × Italy
1 × Poland
3 × United Kingdom
4 × Germany
5 × USA
Collaborated with:N.Bjørner H.Rueß D.Jovanovic B.Dutertre M.Sorea N.Shankar J.M.Rushby G.O.Passmore Y.Ge S.Owre K.Hoder M.P.Bonacina C.Lynch C.M.Wintersteiger Y.Hamadi C.W.Barrett A.Stump G.Hamon S.Kong J.Avigad F.v.Doorn J.v.Raumer I.D.Baxter A.Yahin M.Sant'Anna L.Bier A.Tiwari
Talks about:model (5) satisfi (4) theori (4) effici (4) dpll (4) smt (4) arithmet (3) theorem (3) solver (3) modulo (3)
Person: Leonardo Mendonça de Moura
DBLP: Moura:Leonardo_Mendon=ccedil=a_de
Contributed to:
20152013
2013
20122011
20112010200920092008
200820072007
20082006200520042004
200420032002
1998Wrote 26 papers:
- CADE-2015-MouraKADR #agile #proving #theorem proving
- The Lean Theorem Prover (LMdM, SK, JA, FvD, JvR), pp. 378–388.
- CADE-2013-MouraP
- Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals (LMdM, GOP), pp. 178–192.
- VMCAI-2013-MouraJ #calculus #satisfiability
- A Model-Constructing Satisfiability Calculus (LMdM, DJ), pp. 1–12.
- IJCAR-2012-JovanovicM
- Solving Non-linear Arithmetic (DJ, LMdM), pp. 339–354.
- CADE-2011-JovanovicM #integer #linear
- Cutting to the Chase Solving Linear Integer Arithmetic (DJ, LMdM), pp. 338–353.
- CAV-2011-HoderBM #constraints #fixpoint #named #performance
- μZ — An Efficient Engine for Fixed Points with Constraints (KH, NB, LMdM), pp. 457–462.
- IJCAR-2010-MouraB #debugging #development #reasoning
- Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development (LMdM, NB), pp. 400–411.
- CADE-2009-BonacinaLM #on the #proving #satisfiability #theorem proving
- On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving (MPB, CL, LMdM), pp. 35–50.
- CAV-2009-GeM #modulo theories #quantifier #satisfiability
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories (YG, LMdM), pp. 306–320.
- CAV-2009-WintersteigerHM #approach #concurrent #smt
- A Concurrent Portfolio Approach to SMT Solving (CMW, YH, LMdM), pp. 715–720.
- IJCAR-2008-MouraB #effectiveness #logic #set #using
- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets (LMdM, NB), pp. 410–425.
- IJCAR-2008-MouraB08a
- Engineering DPLL(T) + Saturation (LMdM, NB), pp. 475–490.
- TACAS-2008-MouraB #named #performance #smt
- Z3: An Efficient SMT Solver (LMdM, NB), pp. 337–340.
- CADE-2007-MouraB #performance #smt
- Efficient E-Matching for SMT Solvers (LMdM, NB), pp. 183–198.
- CAV-2007-MouraDS #modulo theories #satisfiability #tutorial
- A Tutorial on Satisfiability Modulo Theories (LMdM, BD, NS), pp. 20–36.
- SMT-2007-MouraB08 #modelling
- Model-based Theory Combination (LMdM, NB), pp. 37–49.
- CAV-2006-DutertreM #performance
- A Fast Linear-Arithmetic Solver for DPLL(T) (BD, LMdM), pp. 81–94.
- CAV-2005-BarrettMS #contest #modulo theories #named #satisfiability
- SMT-COMP: Satisfiability Modulo Theories Competition (CWB, LMdM, AS), pp. 20–23.
- CAV-2004-MouraORRSST
- SAL 2 (LMdM, SO, HR, JMR, NS, MS, AT), pp. 496–500.
- CAV-2004-MouraR #evaluation
- An Experimental Evaluation of Ground Decision Procedures (LMdM, HR), pp. 162–174.
- IJCAR-2004-MouraORRS #deduction #embedded
- The ICS Decision Procedures for Embedded Deduction (LMdM, SO, HR, JMR, NS), pp. 218–222.
- SEFM-2004-HamonMR #generative #model checking #performance #testing
- Generating Efficient Test Sets with a Model Checker (GH, LMdM, JMR), pp. 261–270.
- CAV-2003-MouraRS #bound #induction #model checking #verification
- Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A) (LMdM, HR, MS), pp. 14–26.
- CADE-2002-MouraRS #bound #infinity #lazy evaluation #model checking #proving #theorem proving
- Lazy Theorem Proving for Bounded Model Checking over Infinite Domains (LMdM, HR, MS), pp. 438–455.
- ICSM-1998-BaxterYMSB #abstract syntax tree #clone detection #detection #syntax #using
- Clone Detection Using Abstract Syntax Trees (IDB, AY, LMdM, MS, LB), pp. 368–377.