×

zbMATH — the first resource for mathematics

de Moura, Leonardo

Compute Distance To:
Author ID: de-moura.leonardo Recent zbMATH articles by "de Moura, Leonardo"
Published as: De Moura, Leonardo; Moura, Leonardo; Moura, Leonardo de; de Moura, Leonardo
Homepage: https://leodemoura.github.io/
External Links: MGP · Wikidata · ResearchGate
Documents Indexed: 36 Publications since 2002, including 3 Books

Publications by Year

Citations contained in zbMATH Open

33 Publications have been cited 332 times in 236 Documents Cited by Year
Solving non-linear arithmetic. Zbl 1358.68257
Jovanović, Dejan; de Moura, Leonardo
37
2012
Efficient E-matching for SMT solvers. Zbl 1213.68578
de Moura, Leonardo; Bjørner, Nikolaj
36
2007
Complete instantiation for quantified formulas in satisfiabiliby modulo theories. Zbl 1242.68280
Ge, Yeting; de Moura, Leonardo
29
2009
The Lean theorem prover (system description). Zbl 06515520
de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob
19
2015
Lazy theorem proving for bounded model checking over infinite domains. Zbl 1072.68602
de Moura, Leonardo; Rueß, Harald; Sorea, Maria
19
2002
Efficiently solving quantified bit-vector formulas. Zbl 1284.03212
Wintersteiger, Christoph M.; Hamadi, Youssef; De Moura, Leonardo
16
2013
Model-based theory combination. Zbl 1277.03007
de Moura, Leonardo; Bjørner, Nikolaj
16
2008
Engineering DPLL(T) + saturation. Zbl 1165.68479
de Moura, Leonardo; Bjørner, Nikolaj
15
2008
A model-constructing satisfiability calculus. Zbl 1426.68251
de Moura, Leonardo; Jovanović, Dejan
12
2013
On deciding satisfiability by theorem proving with speculative inferences. Zbl 1243.68265
Bonacina, Maria Paola; Lynch, Christopher A.; de Moura, Leonardo
12
2011
Deciding effectively propositional logic using DPLL and substitution sets. Zbl 1197.03011
Piskac, Ruzica; de Moura, Leonardo; Bjørner, Nikolaj
10
2010
Bounded model checking and induction: From refutation to verification (extended abstract, Category A). Zbl 1278.68199
de Moura, Leonardo; Rueß, Harald; Sorea, Maria
10
2003
Cutting to the chase. Solving linear integer arithmetic. Zbl 1314.90053
Jovanović, Dejan; De Moura, Leonardo
9
2013
The ICS decision procedures for embedded deduction. Zbl 1126.68575
Moura, Leonardo de; Owre, Sam; Rueß, Harald; Rushby, John; Shankar, Natarajan
9
2004
SMT-COMP: Satisfiability modulo theories competition. Zbl 1081.68607
Barrett, Clark; Moura, Leonardo; Stump, Aaron
8
2005
Symbolic automata constraint solving. Zbl 1306.68097
Veanes, Margus; Bjørner, Nikolaj; de Moura, Leonardo
7
2010
Deciding effectively propositional logic using DPLL and substitution sets. Zbl 1165.03320
de Moura, Leonardo; Bjørner, Nikolaj
7
2008
Computation in real closed infinitesimal and transcendental extensions of the rationals. Zbl 1381.68278
de Moura, Leonardo; Passmore, Grant Olney
6
2013
The strategy challenge in SMT solving. Zbl 1383.68084
de Moura, Leonardo; Passmore, Grant Olney
6
2013
Cutting to the chase. Solving linear integer arithmetic. Zbl 1314.90054
Jovanović, Dejan; de Moura, Leonardo
6
2011
SAL 2. Zbl 1103.68644
de Moura, Leonardo; Owre, Sam; Rueß, Harald; Rushby, John; Shankar, N.; Sorea, Maria; Tiwari, Ashish
6
2004
Satisfiability modulo theories: an appetizer. Zbl 1266.03047
de Moura, Leonardo; Bjørner, Nikolaj
5
2009
On deciding satisfiability by \(\mathrm{DPLL}(\Gamma+{\mathcal T})\) and unsound theorem proving. Zbl 1237.68176
Bonacina, Maria Paola; Lynch, Christopher; de Moura, Leonardo
5
2009
Justifying equality. Zbl 1272.68353
De Moura, Leonardo; Rueß, Harald; Shankar, Natarajan
5
2005
An experimental evaluation of ground decision procedures. Zbl 1103.68645
de Moura, Leonardo; Rueß, Harald
5
2004
Bugs, moles and skeletons: symbolic reasoning for software development. Zbl 1291.68377
de Moura, Leonardo; Bjørner, Nikolaj
4
2010
A tutorial on satisfiability modulo theories. Zbl 1135.68563
de Moura, Leonardo; Dutertre, Bruno; Shankar, Natarajan
3
2007
Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005). Zbl 1104.68719
Barrett, Clark; de Moura, Leonardo; Stump, Aaron
3
2005
Automated deduction – CADE 26. 26th international conference on automated deduction, Gothenburg, Sweden, August 6–11, 2017. Proceedings. Zbl 1369.68037
de Moura, Leonardo (ed.)
2
2017
Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006). Zbl 1129.68498
Barrett, Clark; de Moura, Leonardo; Stump, Aaron
2
2007
Congruence closure in intensional type theory. Zbl 06623256
Selsam, Daniel; de Moura, Leonardo
1
2016
Intelligent computer mathematics. 9th international conference, CICM 2016, Bialystok, Poland, July 25–29, 2016. Proceedings. Zbl 1342.68025
Kohlhase, Michael (ed.); Johansson, Moa (ed.); Miller, Bruce (ed.); de Moura, Leonardo (ed.); Tompa, Frank (ed.)
1
2016
Real algebraic strategies for MetiTarski proofs. Zbl 1360.68764
Passmore, Grant Olney; Paulson, Lawrence C.; de Moura, Leonardo
1
2012
Automated deduction – CADE 26. 26th international conference on automated deduction, Gothenburg, Sweden, August 6–11, 2017. Proceedings. Zbl 1369.68037
de Moura, Leonardo (ed.)
2
2017
Congruence closure in intensional type theory. Zbl 06623256
Selsam, Daniel; de Moura, Leonardo
1
2016
Intelligent computer mathematics. 9th international conference, CICM 2016, Bialystok, Poland, July 25–29, 2016. Proceedings. Zbl 1342.68025
Kohlhase, Michael (ed.); Johansson, Moa (ed.); Miller, Bruce (ed.); de Moura, Leonardo (ed.); Tompa, Frank (ed.)
1
2016
The Lean theorem prover (system description). Zbl 06515520
de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob
19
2015
Efficiently solving quantified bit-vector formulas. Zbl 1284.03212
Wintersteiger, Christoph M.; Hamadi, Youssef; De Moura, Leonardo
16
2013
A model-constructing satisfiability calculus. Zbl 1426.68251
de Moura, Leonardo; Jovanović, Dejan
12
2013
Cutting to the chase. Solving linear integer arithmetic. Zbl 1314.90053
Jovanović, Dejan; De Moura, Leonardo
9
2013
Computation in real closed infinitesimal and transcendental extensions of the rationals. Zbl 1381.68278
de Moura, Leonardo; Passmore, Grant Olney
6
2013
The strategy challenge in SMT solving. Zbl 1383.68084
de Moura, Leonardo; Passmore, Grant Olney
6
2013
Solving non-linear arithmetic. Zbl 1358.68257
Jovanović, Dejan; de Moura, Leonardo
37
2012
Real algebraic strategies for MetiTarski proofs. Zbl 1360.68764
Passmore, Grant Olney; Paulson, Lawrence C.; de Moura, Leonardo
1
2012
On deciding satisfiability by theorem proving with speculative inferences. Zbl 1243.68265
Bonacina, Maria Paola; Lynch, Christopher A.; de Moura, Leonardo
12
2011
Cutting to the chase. Solving linear integer arithmetic. Zbl 1314.90054
Jovanović, Dejan; de Moura, Leonardo
6
2011
Deciding effectively propositional logic using DPLL and substitution sets. Zbl 1197.03011
Piskac, Ruzica; de Moura, Leonardo; Bjørner, Nikolaj
10
2010
Symbolic automata constraint solving. Zbl 1306.68097
Veanes, Margus; Bjørner, Nikolaj; de Moura, Leonardo
7
2010
Bugs, moles and skeletons: symbolic reasoning for software development. Zbl 1291.68377
de Moura, Leonardo; Bjørner, Nikolaj
4
2010
Complete instantiation for quantified formulas in satisfiabiliby modulo theories. Zbl 1242.68280
Ge, Yeting; de Moura, Leonardo
29
2009
Satisfiability modulo theories: an appetizer. Zbl 1266.03047
de Moura, Leonardo; Bjørner, Nikolaj
5
2009
On deciding satisfiability by \(\mathrm{DPLL}(\Gamma+{\mathcal T})\) and unsound theorem proving. Zbl 1237.68176
Bonacina, Maria Paola; Lynch, Christopher; de Moura, Leonardo
5
2009
Model-based theory combination. Zbl 1277.03007
de Moura, Leonardo; Bjørner, Nikolaj
16
2008
Engineering DPLL(T) + saturation. Zbl 1165.68479
de Moura, Leonardo; Bjørner, Nikolaj
15
2008
Deciding effectively propositional logic using DPLL and substitution sets. Zbl 1165.03320
de Moura, Leonardo; Bjørner, Nikolaj
7
2008
Efficient E-matching for SMT solvers. Zbl 1213.68578
de Moura, Leonardo; Bjørner, Nikolaj
36
2007
A tutorial on satisfiability modulo theories. Zbl 1135.68563
de Moura, Leonardo; Dutertre, Bruno; Shankar, Natarajan
3
2007
Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006). Zbl 1129.68498
Barrett, Clark; de Moura, Leonardo; Stump, Aaron
2
2007
SMT-COMP: Satisfiability modulo theories competition. Zbl 1081.68607
Barrett, Clark; Moura, Leonardo; Stump, Aaron
8
2005
Justifying equality. Zbl 1272.68353
De Moura, Leonardo; Rueß, Harald; Shankar, Natarajan
5
2005
Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005). Zbl 1104.68719
Barrett, Clark; de Moura, Leonardo; Stump, Aaron
3
2005
The ICS decision procedures for embedded deduction. Zbl 1126.68575
Moura, Leonardo de; Owre, Sam; Rueß, Harald; Rushby, John; Shankar, Natarajan
9
2004
SAL 2. Zbl 1103.68644
de Moura, Leonardo; Owre, Sam; Rueß, Harald; Rushby, John; Shankar, N.; Sorea, Maria; Tiwari, Ashish
6
2004
An experimental evaluation of ground decision procedures. Zbl 1103.68645
de Moura, Leonardo; Rueß, Harald
5
2004
Bounded model checking and induction: From refutation to verification (extended abstract, Category A). Zbl 1278.68199
de Moura, Leonardo; Rueß, Harald; Sorea, Maria
10
2003
Lazy theorem proving for bounded model checking over infinite domains. Zbl 1072.68602
de Moura, Leonardo; Rueß, Harald; Sorea, Maria
19
2002
all top 5

Cited by 443 Authors

12 Bonacina, Maria Paola
11 Weidenbach, Christoph
10 Reynolds, Andrew
9 Tinelli, Cesare
8 Barrett, Clark W.
8 Davenport, James Harold
8 de Moura, Leonardo
8 England, Matthew
7 Ábrahám, Erika
6 Cimatti, Alessandro
6 Fontaine, Pascal
6 Subramani, Krishnan
5 Griggio, Alberto
5 Kremer, Gereon
5 Wintersteiger, Christoph M.
4 Blanchette, Jasmin Christian
4 Bromberger, Martin
4 Echenim, Mnacho
4 Ghilardi, Silvio
4 Jovanović, Dejan
4 Kröning, Daniel
4 Kuncak, Viktor
4 Lynch, Christopher A.
4 Paulson, Lawrence Charles
4 Ranise, Silvio
4 Ringeissen, Christophe
4 Sebastiani, Roberto
4 Stump, Aaron
3 Alberti, Francesco
3 Biere, Armin
3 Bjørner, Nikolaj S.
3 Bruttomesso, Roberto
3 Déharbe, David
3 Giunchiglia, Enrico
3 Johansson, Moa
3 Junges, Sebastian
3 Kaliszyk, Cezary
3 Kruglov, Evgeniĭ Valentinovich
3 Maratea, Marco
3 Marques-Silva, João P.
3 Nicolini, Enrica
3 Passmore, Grant Olney
3 Peltier, Nicolas
3 Rümmer, Philipp
3 Shankar, Natarajan
3 Strichman, Ofer
3 Veanes, Margus
3 Wilson, David J.
2 Armando, Alessandro
2 Becker, Bernd
2 Bradford, Russell J.
2 Bradley, Aaron R.
2 Brain, Martin
2 Bridge, James P.
2 Bright, Curtis
2 Brown, Christopher W.
2 Chakraborty, Supratik
2 Chandrasekaran, Ramaswamy
2 Cockx, Jesper
2 Conchon, Sylvain
2 David, Cristina
2 De Oliveira, Diego Caminha B.
2 Deters, Morgan
2 Dross, Claire
2 Feldman, Yotam M. Y.
2 Ganesh, Vijay
2 Garg, Pranav
2 Gu, Ming
2 Gupta, Ashutosh
2 Hamadi, Youssef
2 Huang, Zongyan
2 Janota, Mikoláš
2 Järvisalo, Matti
2 Jonáš, Martin
2 Katoen, Joost-Pieter
2 Kirchner, Hélène
2 Korovin, Konstantin
2 Kotsireas, Ilias S.
2 Liang, Tianyi
2 Madhusudan, Parthasarathy
2 Meseguer Guaita, José
2 Muñoz, César A.
2 Neider, Daniel
2 Niemetz, Aina
2 Oe, Duckki
2 Ogata, Kazuhiro
2 Ogawa, Mizuhito
2 Oliveras, Albert
2 Padon, Oded
2 Pąk, Karol
2 Plaisted, David Alan
2 Preiner, Mathias
2 Roveri, Marco
2 Rusinowitch, Michaël
2 Sagiv, Mooly
2 Schneider-Kamp, Peter
2 Schulz, Stephan
2 Seshia, Sanjit Arunkumar
2 Sharygina, Natasha
2 Shoham, Sharon
...and 343 more Authors

Citations by Year

Wikidata Timeline

The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.