<dl>

<dt>
<a name="vmcai/demoura13">1</a>
</dt>
<dd>
Leonardo de&nbsp;Moura and Dejan Jovanovi&#x107;.
A model-constructing satisfiability calculus.
In <em>14th International Conference on Verification, Model
Checking, and Abstract Interpretation, VMCAI, Rome, Italy, 2013</em>, 2013.
[&nbsp;<a href="cv-leonardo_bib.html#vmcai/demoura13" onClick="stc(this, 8)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/mcsat.pdf" onClick="stc(this, 9)">.pdf</a>&nbsp;]

</dd>



<dt>
<a name="DBLP:conf/cade/JovanovicM12">3</a>
</dt>
<dd>
Dejan Jovanovi&#x107; and Leonardo de&nbsp;Moura.
Solving non-linear arithmetic.
In <em>Automated Reasoning - 6th International Joint Conference,
IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings</em>, volume 7364 of
<em>Lecture Notes in Computer Science</em>, pages 339-354. Springer, 2012.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:conf/cade/JovanovicM12" onClick="stc(this, 12)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/IJCAR2012.pdf" onClick="stc(this, 13)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="MSR:techreport:nonlinear12">4</a>
</dt>
<dd>
Dejan Jovanovi&#x107; and Leonardo de&nbsp;Moura.
Solving non-linear arithmetic.
Technical Report MSR-TR-2012-20, Microsoft Research, 2012.
[&nbsp;<a href="cv-leonardo_bib.html#MSR:techreport:nonlinear12" onClick="stc(this, 14)">bib</a>&nbsp;|
<a href="http://research.microsoft.com/apps/pubs/default.aspx?id=159549" onClick="stc(this, 15)">http</a>&nbsp;]

</dd>


<dt>
<a name="whd12">6</a>
</dt>
<dd>
Christoph Wintersteiger, Youssef Hamadi, and Leonardo de&nbsp;Moura.
Efficiently solving quantified bit-vector formulas.
<em>Formal Methods in System Design</em>, 2012.
[&nbsp;<a href="cv-leonardo_bib.html#whd12" onClick="stc(this, 18)">bib</a>&nbsp;|
<a href="http://dx.doi.org/10.1007/s10703-012-0156-2" onClick="stc(this, 19)">http</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/ufbv_journal.pdf" onClick="stc(this, 20)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="tractability">7</a>
</dt>
<dd>
Nikolaj Bj&oslash;rner and Leonardo de&nbsp;Moura.
Tractability and Modern Satisfiability Modulo Theories Solvers.
In <em>Handbook of Tractability</em>. Cambridge University Press, 2012.
[&nbsp;<a href="cv-leonardo_bib.html#tractability" onClick="stc(this, 21)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/tractability.pdf" onClick="stc(this, 22)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:conf/cav/HoderBM11">8</a>
</dt>
<dd>
Krystof Hoder, Nikolaj Bj&oslash;rner, and Leonardo de&nbsp;Moura.
muZ - an efficient engine for fixed points with constraints.
In <em>Computer Aided Verification - 23rd International Conference,
CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings</em>, volume 6806 of
<em>Lecture Notes in Computer Science</em>, pages 457-462, 2011.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:conf/cav/HoderBM11" onClick="stc(this, 23)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/muze.pdf" onClick="stc(this, 24)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:journals/cacm/MouraB11">9</a>
</dt>
<dd>
Leonardo de&nbsp;Moura and Nikolaj Bj&oslash;rner.
Satisfiability modulo theories: introduction and applications.
<em>Commun. ACM</em>, 54(9):69-77, 2011.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:journals/cacm/MouraB11" onClick="stc(this, 25)">bib</a>&nbsp;|
<a href="http://dl.acm.org/citation.cfm?id=1995394" onClick="stc(this, 26)">http</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:conf/cade/JovanovicM11">10</a>
</dt>
<dd>
Dejan Jovanovi&#x107; and Leonardo de&nbsp;Moura.
Cutting to the chase solving linear integer arithmetic.
In <em>Automated Deduction - CADE-23 - 23rd International Conference
on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011.
Proceedings</em>, volume 6803 of <em>Lecture Notes in Computer Science</em>, pages
338-353. Springer, 2011.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:conf/cade/JovanovicM11" onClick="stc(this, 27)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/cutsat.pdf" onClick="stc(this, 28)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:journals/jar/BonacinaLM11">11</a>
</dt>
<dd>
Maria&nbsp;Paola Bonacina, Christopher Lynch, and Leonardo de&nbsp;Moura.
On deciding satisfiability by theorem proving with speculative
inferences.
<em>J. Autom. Reasoning</em>, 47(2):161-189, 2011.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:journals/jar/BonacinaLM11" onClick="stc(this, 29)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/JAR2010dpllSPsi.pdf" onClick="stc(this, 30)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:conf/cade/MouraB10">12</a>
</dt>
<dd>
Leonardo de&nbsp;Moura and Nikolaj Bj&oslash;rner.
Bugs, moles and skeletons: Symbolic reasoning for software
development.
In <em>Automated Reasoning, 5th International Joint Conference,
IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings</em>, volume 6173 of
<em>Lecture Notes in Computer Science</em>, pages 400-411. Springer, 2010.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:conf/cade/MouraB10" onClick="stc(this, 31)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/ijcar10.pdf" onClick="stc(this, 32)">.pdf</a>&nbsp;]

</dd>



<dt>
<a name="DBLP:journals/jar/PiskacMB10">14</a>
</dt>
<dd>
Ruzica Piskac, Leonardo de&nbsp;Moura, and Nikolaj Bj&oslash;rner.
Deciding effectively propositional logic using DPLL and
substitution sets.
<em>J. Autom. Reasoning</em>, 44(4):401-424, 2010.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:journals/jar/PiskacMB10" onClick="stc(this, 35)">bib</a>&nbsp;|
<a href="http://www.springerlink.com/content/p54255p52430242t/" onClick="stc(this, 36)">http</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:conf/fmcad/WintersteigerHM10">15</a>
</dt>
<dd>
Christoph&nbsp;M. Wintersteiger, Youssef Hamadi, and Leonardo de&nbsp;Moura.
Efficiently solving quantified bit-vector formulas.
In <em>Proceedings of 10th International Conference on Formal
Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October
20-23</em>, pages 239-246. IEEE, 2010.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:conf/fmcad/WintersteigerHM10" onClick="stc(this, 37)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/fmcad10.pdf" onClick="stc(this, 38)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:conf/fmcad/MouraB09">16</a>
</dt>
<dd>
Leonardo de&nbsp;Moura and Nikolaj Bj&oslash;rner.
Generalized, efficient array decision procedures.
In <em>Proceedings of 9th International Conference on Formal Methods
in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas,
USA</em>, pages 45-52. IEEE, 2009.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:conf/fmcad/MouraB09" onClick="stc(this, 39)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/fmcad09.pdf" onClick="stc(this, 40)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:conf/formats/BjornerM09">17</a>
</dt>
<dd>
Nikolaj Bj&oslash;rner and Leonardo de&nbsp;Moura.
Tapas: Theory combinations and practical applications.
In <em>Formal Modeling and Analysis of Timed Systems, 7th
International Conference, FORMATS 2009, Budapest, Hungary, September 14-16,
2009. Proceedings</em>, volume 5813 of <em>Lecture Notes in Computer Science</em>,
pages 1-6. Springer, 2009.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:conf/formats/BjornerM09" onClick="stc(this, 41)">bib</a>&nbsp;|
<a href="http://www.springerlink.com/content/u510v392760624q5/" onClick="stc(this, 42)">http</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:conf/sbmf/MouraB09">18</a>
</dt>
<dd>
Leonardo de&nbsp;Moura and Nikolaj Bj&oslash;rner.
Satisfiability modulo theories: An appetizer.
In <em>Formal Methods: Foundations and Applications, 12th Brazilian
Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009,
Revised Selected Papers</em>, volume 5902 of <em>Lecture Notes in Computer
Science</em>, pages 23-36. Springer, 2009.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:conf/sbmf/MouraB09" onClick="stc(this, 43)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/sbmf09.pdf" onClick="stc(this, 44)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:conf/cade/BonacinaLM09">19</a>
</dt>
<dd>
Maria&nbsp;Paola Bonacina, Christopher Lynch, and Leonardo de&nbsp;Moura.
On deciding satisfiability by DPLL(&Gamma;+T) and unsound theorem
proving.
In <em>Automated Deduction - CADE-22, 22nd International Conference
on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings</em>,
volume 5663 of <em>Lecture Notes in Computer Science</em>, pages 35-50.
Springer, 2009.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:conf/cade/BonacinaLM09" onClick="stc(this, 45)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/cade09.pdf" onClick="stc(this, 46)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:conf/cav/GeM09">20</a>
</dt>
<dd>
Yeting Ge and Leonardo de&nbsp;Moura.
Complete instantiation for quantified formulas in satisfiabiliby
modulo theories.
In <em>Computer Aided Verification, 21st International Conference,
CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings</em>, volume 5643
of <em>Lecture Notes in Computer Science</em>, pages 306-320. Springer, 2009.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:conf/cav/GeM09" onClick="stc(this, 47)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/ci.pdf" onClick="stc(this, 48)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:conf/cav/WintersteigerHM09">21</a>
</dt>
<dd>
Christoph&nbsp;M. Wintersteiger, Youssef Hamadi, and Leonardo de&nbsp;Moura.
A concurrent portfolio approach to SMT solving.
In <em>Computer Aided Verification, 21st International Conference,
CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings</em>, volume 5643
of <em>Lecture Notes in Computer Science</em>, pages 715-720. Springer, 2009.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:conf/cav/WintersteigerHM09" onClick="stc(this, 49)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/parallel_z3.pdf" onClick="stc(this, 50)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:conf/synasc/PassmoreM09">22</a>
</dt>
<dd>
Grant&nbsp;Olney Passmore and Leonardo de&nbsp;Moura.
Superfluous S-polynomials in strategy-independent groebner bases.
In <em>11th International Symposium on Symbolic and Numeric
Algorithms for Scientific Computing, SYNASC 2009, Timisoara, Romania,
September 26-29, 2009</em>, pages 45-53. IEEE Computer Society, 2009.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:conf/synasc/PassmoreM09" onClick="stc(this, 51)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/synasc.pdf" onClick="stc(this, 52)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="BjornerDeMoura2009">23</a>
</dt>
<dd>
Nikolaj Bj&oslash;rner and Leonardo de&nbsp;Moura.
<em>z</em>3<sup>10</sup>: Applications, enablers, challenges and directions.
In <em>Sixth International Workshop on Constraints in Formal
Verification Grenoble, France</em>, 2009.
[&nbsp;<a href="cv-leonardo_bib.html#BjornerDeMoura2009" onClick="stc(this, 53)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/cfv09.pdf" onClick="stc(this, 54)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="deMouraPassmore09">24</a>
</dt>
<dd>
Leonardo de&nbsp;Moura and Grant&nbsp;Olney Passmore.
On locally minimal nullstellensatz proofs.
In <em>7th International Workshop on Satisfiability Modulo Theories,
SMT, Montreal, Canada</em>, 2009.
[&nbsp;<a href="cv-leonardo_bib.html#deMouraPassmore09" onClick="stc(this, 55)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/SMT-09.pdf" onClick="stc(this, 56)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="deMouraPassmore09ext">25</a>
</dt>
<dd>
Leonardo de&nbsp;Moura and Grant&nbsp;Olney Passmore.
On locally minimal nullstellensatz proofs.
Technical Report MSR-TR-2009-90, Microsoft Research, 2009.
[&nbsp;<a href="cv-leonardo_bib.html#deMouraPassmore09ext" onClick="stc(this, 57)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/MSR-TR-2009-90.pdf" onClick="stc(this, 58)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="PassmoreDeMoura09">26</a>
</dt>
<dd>
Grant&nbsp;Olney Passmore and Leonardo de&nbsp;Moura.
Universality of polynomial positivity and a variant of Hilbert's
17th problem.
In <em>Automated Deduction: Decidability, Complexity, Tractability,
ADDCT'09, Montreal, Canada</em>, 2009.
[&nbsp;<a href="cv-leonardo_bib.html#PassmoreDeMoura09" onClick="stc(this, 59)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/addct-09.pdf" onClick="stc(this, 60)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="MSR:techreport:EPR08">27</a>
</dt>
<dd>
Ruzica Piskac, Leonardo de&nbsp;Moura, and Nikolaj Bj&oslash;rner.
Deciding effectively propositional logic with equality.
Technical Report MSR-TR-2008-181, Microsoft Research, 2008.
[&nbsp;<a href="cv-leonardo_bib.html#MSR:techreport:EPR08" onClick="stc(this, 61)">bib</a>&nbsp;|
<a href="http://research.microsoft.com/apps/pubs/default.aspx?id=76532" onClick="stc(this, 62)">http</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:conf/cade/MouraB08">28</a>
</dt>
<dd>
Leonardo de&nbsp;Moura and Nikolaj Bj&oslash;rner.
Deciding effectively propositional logic using DPLL and
substitution sets.
In <em>Automated Reasoning, 4th International Joint Conference,
IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings</em>, volume 5195
of <em>Lecture Notes in Computer Science</em>, pages 410-425. Springer, 2008.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:conf/cade/MouraB08" onClick="stc(this, 63)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/epr.pdf" onClick="stc(this, 64)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:conf/cade/MouraB08a">29</a>
</dt>
<dd>
Leonardo de&nbsp;Moura and Nikolaj Bj&oslash;rner.
Engineering DPLL(T) + Saturation.
In <em>Automated Reasoning, 4th International Joint Conference,
IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings</em>, volume 5195
of <em>Lecture Notes in Computer Science</em>, pages 475-490. Springer, 2008.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:conf/cade/MouraB08a" onClick="stc(this, 65)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/z3spc.pdf" onClick="stc(this, 66)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:conf/lpar/MouraB08">30</a>
</dt>
<dd>
Leonardo de&nbsp;Moura and Nikolaj Bj&oslash;rner.
Proofs and refutations, and Z3.
In <em>Proceedings of the LPAR 2008 Workshops, Knowledge Exchange:
Automated Provers and Proof Assistants, and the 7th International Workshop on
the Implementation of Logics, Doha, Qatar, November 22, 2008</em>, volume 418 of
<em>CEUR Workshop Proceedings</em>. CEUR-WS.org, 2008.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:conf/lpar/MouraB08" onClick="stc(this, 67)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/iwil08.pdf" onClick="stc(this, 68)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:conf/tacas/MouraB08">31</a>
</dt>
<dd>
Leonardo de&nbsp;Moura and Nikolaj Bj&oslash;rner.
Z3: An efficient SMT solver.
In <em>Tools and Algorithms for the Construction and Analysis of
Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint
European Conferences on Theory and Practice of Software, ETAPS 2008,
Budapest, Hungary, March 29-April 6, 2008. Proceedings</em>, volume 4963 of <em>
Lecture Notes in Computer Science</em>, pages 337-340. Springer, 2008.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:conf/tacas/MouraB08" onClick="stc(this, 69)">bib</a>&nbsp;|
<a href="http://research.microsoft.com/projects/z3/z3.pdf" onClick="stc(this, 70)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:journals/entcs/MouraB08">32</a>
</dt>
<dd>
Leonardo de&nbsp;Moura and Nikolaj Bj&oslash;rner.
Model-based theory combination.
<em>Electr. Notes Theor. Comput. Sci.</em>, 198(2):37-49, 2008.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:journals/entcs/MouraB08" onClick="stc(this, 71)">bib</a>&nbsp;|
<a href="http://research.microsoft.com/projects/z3/smt07.pdf" onClick="stc(this, 72)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="LPAR:Join:08">33</a>
</dt>
<dd>
Nikolaj Bj&oslash;rner, Bruno Dutertre, and Leonardo de&nbsp;Moura.
Accelerating lemma learning using joins - DPPL(Join).
In <em>15th International Conference on Logic for Programming
Artificial Intelligence and Reasoning, LPAR'08</em>, 2008.
[&nbsp;<a href="cv-leonardo_bib.html#LPAR:Join:08" onClick="stc(this, 73)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/joins.pdf" onClick="stc(this, 74)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="BjornerDeMouraTillmann09">34</a>
</dt>
<dd>
Nikolaj Bj&oslash;rner, Leonardo de&nbsp;Moura, and Nikolai Tillmann.
Satisfiability modulo bit-precise theories for program exploration.
In <em>Fifth International Workshop on Constraints in Formal
Verification, (CFV'08), Sydney, Australia</em>, 2008.
[&nbsp;<a href="cv-leonardo_bib.html#BjornerDeMouraTillmann09" onClick="stc(this, 75)">bib</a>&nbsp;|
<a href=" http://research.microsoft.com/en-us/um/people/leonardo/files/smbpex.pdf" onClick="stc(this, 76)">.pdf</a>&nbsp;]

</dd>


<dt>
<a name="DBLP:conf/cade/MouraB07">35</a>
</dt>
<dd>
Leonardo de&nbsp;Moura and Nikolaj Bj&oslash;rner.
Efficient E-Matching for SMT solvers.
In <em>Automated Deduction - CADE-21, 21st International Conference
on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings</em>,
volume 4603 of <em>Lecture Notes in Computer Science</em>, pages 183-198.
Springer, 2007.
[&nbsp;<a href="cv-leonardo_bib.html#DBLP:conf/cade/MouraB07" onClick="stc(this, 77)">bib</a>&nbsp;|
<a href="http://research.microsoft.com/projects/z3/cade07.pdf" onClick="stc(this, 78)">.pdf</a>&nbsp;]

</dd>

</dl>

Last edited Dec 30, 2012 at 7:28 AM by leodemoura, version 1

Comments

No comments yet.