Publications

cv-leonardo.bib

@inproceedings{fmcad13/dbdm13,
  author = {Dejan Jovanovi\'{c} and Clark Barrett and Leonardo de Moura},
  title = {The Design and Implementation of the Model Constructing Satisfiability Calculus},
  booktitle = {Proceedings of 13th International Conference on Formal Methods
               in Computer-Aided Design, FMCAD 2013, 20-23 October 2013,
               Porland, Oregon, USA},
  year = {2013}
}
@inproceedings{cade24/dmp13,
  author = {Leonardo de Moura and Grant Passmore},
  title = {Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals},
  booktitle = {Automated Deduction - CADE-24, 24th International Conference
               on Automated Deduction, Lake Placid, New York, June 9-14, 2013,
               Proceedings},
  year = {2013},
  documenturl = {http://z3.codeplex.com/wikipage?title=CADE24}
}
@article{cutsat/jar2013,
  author = {Dejan Jovanovi\'{c} and
            Leonardo de Moura},
  title = {Cutting to the Chase: Solving Linear Integer Arithmetic (to appear)},
  journal = {Journal Automated Reasoning},
  year = {2013},
  documenturl = {http://research.microsoft.com/en-us/um/people/leonardo/files/cutsat-jar2013.pdf}
}
@inbook{mcsat,
  title = ,
  author = { Leonardo de Moura and Grant Passmore },
  booktitle = { Automated Reasoning and Mathematics: Essays in Memory of William McCune },
  year = {2013},
  series = { Lecture Notes in Artificial Intelligence },
  publisher = {Springer},
  volume = { 7788 },
  documenturl = {http://research.microsoft.com/en-us/um/people/leonardo/files/smt-strategy.pdf}
}
@inproceedings{vmcai/demoura13,
  author = {Leonardo de Moura and Dejan Jovanovi\'{c} },
  title = { A Model-Constructing Satisfiability Calculus },
  booktitle = {14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI, Rome, Italy, 2013},
  year = {2013},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/mcsat.pdf}
}
@inproceedings{DBLP:conf/cav/HoderBM11,
  author = {Krystof Hoder and
               Nikolaj Bj{\o}rner and
               Leonardo de Moura},
  title = { {muZ} - An Efficient Engine for Fixed Points with
               Constraints},
  booktitle = {Computer Aided Verification - 23rd International Conference,
               CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
  year = {2011},
  pages = {457-462},
  ee = {http://dx.doi.org/10.1007/978-3-642-22110-1_36},
  series = {Lecture Notes in Computer Science},
  volume = {6806},
  documenturl = {http://research.microsoft.com/en-us/um/people/leonardo/files/muze.pdf}
}
@article{DBLP:journals/cacm/MouraB11,
  author = {Leonardo de Moura and
               Nikolaj Bj{\o}rner},
  title = {Satisfiability modulo theories: introduction and applications},
  journal = {Commun. ACM},
  volume = {54},
  number = {9},
  year = {2011},
  pages = {69-77},
  documenturl = {http://dl.acm.org/citation.cfm?id=1995394},
  documenturl = {http://cacm.acm.org/magazines/2011/9/122785-satisfiability-modulo-theories/fulltext}
}
@inproceedings{DBLP:conf/cade/MouraB10,
  author = {Leonardo de Moura and
               Nikolaj Bj{\o}rner},
  title = {Bugs, Moles and Skeletons: Symbolic Reasoning for Software
               Development},
  booktitle = {Automated Reasoning, 5th International Joint Conference,
               IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings},
  year = {2010},
  pages = {400-411},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6173},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/ijcar10.pdf}
}
@inproceedings{DBLP:conf/lpar/VeanesBM10,
  author = {Margus Veanes and
               Nikolaj Bj{\o}rner and
               Leonardo de Moura},
  title = {Symbolic Automata Constraint Solving},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning
               - 17th International Conference, LPAR-17, Yogyakarta, Indonesia,
               October 10-15, 2010. Proceedings},
  year = {2010},
  pages = {640-654},
  series = {Lecture Notes in Computer Science},
  volume = {6397},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/lpar2010.pdf}
}
@article{DBLP:journals/jar/PiskacMB10,
  author = {Ruzica Piskac and
               Leonardo de Moura and
               Nikolaj Bj{\o}rner},
  title = {Deciding Effectively Propositional Logic Using {DPLL} and
               Substitution Sets},
  journal = {J. Autom. Reasoning},
  volume = {44},
  number = {4},
  year = {2010},
  pages = {401-424},
  documenturl = {http://www.springerlink.com/content/p54255p52430242t/}
}
@techreport{MSR:techreport:EPR08,
  author = {Ruzica Piskac and
               Leonardo de Moura and
               Nikolaj Bj{\o}rner},
  title = {Deciding Effectively Propositional Logic with Equality},
  year = {2008},
  number = {MSR-TR-2008-181},
  institution = { {Microsoft Research} },
  documenturl = {http://research.microsoft.com/apps/pubs/default.aspx?id=76532}
}
@inproceedings{DBLP:conf/fmcad/MouraB09,
  author = {Leonardo de Moura and
               Nikolaj Bj{\o}rner},
  title = {Generalized, efficient array decision procedures},
  year = {2009},
  pages = {45-52},
  booktitle = {Proceedings of 9th International Conference on Formal Methods
               in Computer-Aided Design, FMCAD 2009, 15-18 November 2009,
               Austin, Texas, USA},
  publisher = {IEEE},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/fmcad09.pdf}
}
@inproceedings{DBLP:conf/formats/BjornerM09,
  author = {Nikolaj Bj{\o}rner and
               Leonardo de Moura},
  title = {Tapas: Theory Combinations and Practical Applications},
  year = {2009},
  pages = {1-6},
  booktitle = {Formal Modeling and Analysis of Timed Systems, 7th International
               Conference, FORMATS 2009, Budapest, Hungary, September 14-16,
               2009. Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5813},
  documenturl = {http://www.springerlink.com/content/u510v392760624q5/}
}
@inproceedings{DBLP:conf/sbmf/MouraB09,
  author = {Leonardo de Moura and
               Nikolaj Bj{\o}rner},
  title = {Satisfiability Modulo Theories: An Appetizer},
  year = {2009},
  pages = {23-36},
  booktitle = {Formal Methods: Foundations and Applications, 12th Brazilian
               Symposium on Formal Methods, SBMF 2009, Gramado, Brazil,
               August 19-21, 2009, Revised Selected Papers},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5902},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/sbmf09.pdf}
}
@inproceedings{DBLP:conf/cade/MouraB08,
  author = {Leonardo de Moura and
               Nikolaj Bj{\o}rner},
  title = {Deciding Effectively Propositional Logic Using {DPLL} and
               Substitution Sets},
  year = {2008},
  pages = {410-425},
  booktitle = {Automated Reasoning, 4th International Joint Conference,
               IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5195},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/epr.pdf}
}
@inproceedings{DBLP:conf/cade/MouraB08a,
  author = {Leonardo de Moura and
               Nikolaj Bj{\o}rner},
  title = { {Engineering DPLL(T) + Saturation} },
  year = {2008},
  pages = {475-490},
  booktitle = {Automated Reasoning, 4th International Joint Conference,
               IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5195},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/z3spc.pdf}
}
@inproceedings{DBLP:conf/lpar/MouraB08,
  author = {Leonardo de Moura and
               Nikolaj Bj{\o}rner},
  title = {Proofs and Refutations, and {Z3}},
  year = {2008},
  booktitle = {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},
  publisher = {CEUR-WS.org},
  series = {CEUR Workshop Proceedings},
  volume = {418},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/iwil08.pdf}
}
@inproceedings{DBLP:conf/tacas/MouraB08,
  author = {Leonardo de Moura and
               Nikolaj Bj{\o}rner},
  title = { {Z3}: An Efficient {SMT} Solver},
  year = {2008},
  pages = {337-340},
  booktitle = {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},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4963},
  documenturl = {http://research.microsoft.com/projects/z3/z3.pdf}
}
@article{DBLP:journals/entcs/MouraB08,
  author = {Leonardo de Moura and
               Nikolaj Bj{\o}rner},
  title = {Model-based Theory Combination},
  journal = {Electr. Notes Theor. Comput. Sci.},
  volume = {198},
  number = {2},
  year = {2008},
  pages = {37-49},
  ee = {http://dx.doi.org/10.1016/j.entcs.2008.04.079},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  documenturl = {http://research.microsoft.com/projects/z3/smt07.pdf}
}
@inproceedings{DBLP:conf/cade/MouraB07,
  author = {Leonardo de Moura and
               Nikolaj Bj{\o}rner},
  title = {Efficient {E-Matching} for {SMT} Solvers},
  year = {2007},
  pages = {183-198},
  booktitle = {Automated Deduction - CADE-21, 21st International Conference
               on Automated Deduction, Bremen, Germany, July 17-20, 2007,
               Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4603},
  documenturl = {http://research.microsoft.com/projects/z3/cade07.pdf}
}
@inproceedings{DBLP:conf/aisc/PassmorePM12,
  author = {Grant Olney Passmore and
               Lawrence C. Paulson and
               Leonardo de Moura},
  title = {Real Algebraic Strategies for {MetiTarski} Proofs},
  year = {2012},
  pages = {358-370},
  booktitle = {Intelligent Computer Mathematics - 11th International Conference,
               AISC 2012, 19th Symposium, Calculemus 2012, 5th International
               Workshop, DML 2012, 11th International Conference, MKM 2012,
               Systems and Projects, Held as Part of CICM 2012, Bremen,
               Germany, July 8-13, 2012. Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {7362},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/CICM2012.pdf}
}
@inproceedings{DBLP:conf/cade/JovanovicM12,
  author = {Dejan Jovanovi\'{c} and
               Leonardo de Moura},
  title = {Solving Non-linear Arithmetic},
  year = {2012},
  pages = {339-354},
  booktitle = {Automated Reasoning - 6th International Joint Conference,
               IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {7364},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/IJCAR2012.pdf}
}
@techreport{MSR:techreport:nonlinear12,
  author = {Dejan Jovanovi\'{c} and
               Leonardo de Moura},
  title = {Solving Non-linear Arithmetic},
  year = {2012},
  number = {MSR-TR-2012-20},
  institution = { {Microsoft Research} },
  documenturl = {http://research.microsoft.com/apps/pubs/default.aspx?id=159549}
}
@inproceedings{DBLP:conf/cade/JovanovicM11,
  author = {Dejan Jovanovi\'{c} and
               Leonardo de Moura},
  title = {Cutting to the Chase Solving Linear Integer Arithmetic},
  year = {2011},
  pages = {338-353},
  booktitle = {Automated Deduction - CADE-23 - 23rd International Conference
               on Automated Deduction, Wroclaw, Poland, July 31 - August
               5, 2011. Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6803},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/cutsat.pdf}
}
@article{DBLP:journals/jar/BonacinaLM11,
  author = {Maria Paola Bonacina and
               Christopher Lynch and
               Leonardo de Moura},
  title = {On Deciding Satisfiability by Theorem Proving with Speculative
               Inferences},
  journal = {J. Autom. Reasoning},
  volume = {47},
  number = {2},
  year = {2011},
  pages = {161-189},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/JAR2010dpllSPsi.pdf}
}
@inproceedings{DBLP:conf/fmcad/WintersteigerHM10,
  author = {Christoph M. Wintersteiger and
               Youssef Hamadi and
               Leonardo de Moura},
  title = {Efficiently solving quantified bit-vector formulas},
  year = {2010},
  pages = {239-246},
  booktitle = {Proceedings of 10th International Conference on Formal Methods
               in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland,
               October 20-23},
  publisher = {IEEE},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/fmcad10.pdf}
}
@inproceedings{DBLP:conf/cade/BonacinaLM09,
  author = {Maria Paola Bonacina and
               Christopher Lynch and
               Leonardo de Moura},
  title = {On Deciding Satisfiability by {DPLL($\Gamma$+T)} and Unsound
               Theorem Proving},
  year = {2009},
  pages = {35-50},
  booktitle = {Automated Deduction - CADE-22, 22nd International Conference
               on Automated Deduction, Montreal, Canada, August 2-7, 2009.
               Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5663},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/cade09.pdf}
}
@inproceedings{DBLP:conf/cav/GeM09,
  author = {Yeting Ge and
               Leonardo de Moura},
  title = {Complete Instantiation for Quantified Formulas in Satisfiabiliby
               Modulo Theories},
  year = {2009},
  pages = {306-320},
  booktitle = {Computer Aided Verification, 21st International Conference,
               CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5643},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/ci.pdf}
}
@inproceedings{GeM09ext,
  author = {Yeting Ge and
               Leonardo de Moura},
  title = {Complete Instantiation for Quantified Formulas in Satisfiabiliby
               Modulo Theories (extended version)},
  year = {2009},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/citr09.pdf}
}
@inproceedings{DBLP:conf/cav/WintersteigerHM09,
  author = {Christoph M. Wintersteiger and
               Youssef Hamadi and
               Leonardo de Moura},
  title = {A Concurrent Portfolio Approach to {SMT} Solving},
  year = {2009},
  pages = {715-720},
  booktitle = {Computer Aided Verification, 21st International Conference,
               CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5643},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/parallel_z3.pdf}
}
@inproceedings{DBLP:conf/synasc/PassmoreM09,
  author = {Grant Olney Passmore and
               Leonardo de Moura},
  title = {Superfluous {S-polynomials} in Strategy-Independent Groebner
               Bases},
  year = {2009},
  pages = {45-53},
  booktitle = {11th International Symposium on Symbolic and Numeric Algorithms
               for Scientific Computing, SYNASC 2009, Timisoara, Romania,
               September 26-29, 2009},
  publisher = {IEEE Computer Society},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/synasc.pdf}
}
@inproceedings{DBLP:conf/cav/MouraDS07,
  author = {Leonardo de Moura and
               Bruno Dutertre and
               Natarajan Shankar},
  title = {A Tutorial on Satisfiability Modulo Theories},
  year = {2007},
  pages = {20-36},
  booktitle = {Computer Aided Verification, 19th International Conference,
               CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4590},
  documenturl = {http://www.springerlink.com/content/11r20jq883677834}
}
@article{DBLP:journals/fmsd/BarrettMS07,
  author = {Clark W. Barrett and
               Leonardo de Moura and
               Aaron Stump},
  title = {Design and results of the 2nd annual satisfiability modulo
               theories competition ({SMT-COMP} 2006)},
  journal = {Formal Methods in System Design},
  volume = {31},
  number = {3},
  year = {2007},
  pages = {221-239},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/smtcomp06.pdf}
}
@inproceedings{DBLP:conf/cav/DutertreM06,
  author = {Bruno Dutertre and
               Leonardo de Moura},
  title = {A Fast Linear-Arithmetic Solver for {DPLL(T)}},
  year = {2006},
  pages = {81-94},
  booktitle = {Computer Aided Verification, 18th International Conference,
               CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4144},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/cav06.pdf}
}
@inproceedings{DBLP:conf/cav/BarrettMS05,
  author = {Clark W. Barrett and
               Leonardo de Moura and
               Aaron Stump},
  title = { {SMT-COMP}: Satisfiability Modulo Theories Competition },
  year = {2005},
  pages = {20-23},
  booktitle = {Computer Aided Verification, 17th International Conference,
               CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3576},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/smtcomp05_short_paper.pdf}
}
@article{BdMS05-JAR,
  author = {Clark Barrett and Leonardo de Moura and Aaron Stump},
  doi = {10.1007/s10817-006-9026-1},
  journal = {Journal of Automated Reasoning},
  month = nov,
  number = {4},
  pages = {373--390},
  posted-at = {2011-02-08 17:43:04},
  priority = {2},
  publisher = {Springer Netherlands},
  title = {Design and Results of the First Satisfiability Modulo Theories Competition ({SMT-COMP} 2005)},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/smtcomp_jar.pdf},
  volume = {35},
  year = {2005}
}
@article{DBLP:journals/entcs/MouraRS05,
  author = {Leonardo de Moura and
               Harald Rue{\ss} and
               Natarajan Shankar},
  title = {Justifying Equality},
  journal = {Electr. Notes Theor. Comput. Sci.},
  volume = {125},
  number = {3},
  year = {2005},
  pages = {69-85},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/equality.pdf}
}
@inproceedings{DBLP:conf/cav/MouraR04,
  author = {Leonardo de Moura and
               Harald Rue{\ss}},
  title = {An Experimental Evaluation of Ground Decision Procedures},
  year = {2004},
  pages = {162-174},
  booktitle = {Computer Aided Verification, 16th International Conference,
               CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3114},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/gdp.pdf}
}
@inproceedings{DBLP:conf/cav/MouraORRSST04,
  author = {Leonardo de Moura and Sam Owre and Harald Rue{\ss} and John M. Rushby and Natarajan Shankar and Maria Sorea and Ashish Tiwari},
  title = { {SAL 2} },
  year = {2004},
  pages = {496-500},
  booktitle = {Computer Aided Verification, 16th International Conference,
               CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3114},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/sal2.pdf}
}
@inproceedings{DBLP:conf/cade/MouraORRS04,
  author = {Leonardo de Moura and Sam Owre and Harald Rue{\ss} and John M. Rushby and Natarajan Shankar},
  title = {The {ICS} Decision Procedures for Embedded Deduction},
  year = {2004},
  pages = {218-222},
  booktitle = {Automated Reasoning - Second International Joint Conference,
               IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3097},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/ics.pdf}
}
@inproceedings{DBLP:conf/sefm/HamonMR04,
  author = {Gr{\'e}goire Hamon and
               Leonardo de Moura and
               John M. Rushby},
  title = {Generating Efficient Test Sets with a Model Checker},
  year = {2004},
  pages = {261-270},
  booktitle = {2nd International Conference on Software Engineering and
               Formal Methods (SEFM 2004), 28-30 September 2004, Beijing,
               China},
  publisher = {IEEE Computer Society},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/testgen.pdf}
}
@inproceedings{DBLP:conf/cav/MouraRS03,
  author = {Leonardo de Moura and
               Harald Rue{\ss} and
               Maria Sorea},
  title = {Bounded Model Checking and Induction: From Refutation to
               Verification},
  year = {2003},
  pages = {14-26},
  booktitle = {Computer Aided Verification, 15th International Conference,
               CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {2725},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/cav03.pdf}
}
@inproceedings{DBLP:conf/wsc/RuessM03,
  author = {Harald Rue{\ss} and
               Leonardo de Moura},
  title = {From simulation to verification (and back)},
  year = {2003},
  pages = {888-896},
  booktitle = {Proceedings of the 35th Winter Simulation Conference: Driving
               Innovation,  New Orleans, Louisiana, USA, December 7-10,
               2003},
  publisher = {ACM},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/wsc03.pdf}
}
@inproceedings{DBLP:conf/cade/MouraRS02,
  author = {Leonardo de Moura and
               Harald Rue{\ss} and
               Maria Sorea},
  title = {Lazy Theorem Proving for Bounded Model Checking over Infinite
               Domains},
  year = {2002},
  pages = {438-455},
  booktitle = {Automated Deduction - CADE-18, 18th International Conference
               on Automated Deduction, Copenhagen, Denmark, July 27-30,
               2002, Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {2392},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/cade02.pdf}
}
@inproceedings{DBLP:conf/icsm/BaxterYMSB98,
  author = {Ira D. Baxter and
               Andrew Yahin and
               Leonardo de Moura and
               Marcelo Sant'Anna and
               Lorraine Bier},
  title = {Clone Detection Using Abstract Syntax Trees},
  booktitle = {International Conference on Software Maintenance ({ICSM'98}), Bethesda, Maryland, USA},
  year = {1998},
  pages = {368-377},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/ICSM98.pdf}
}
@techreport{SRI:yices:tool,
  author = { Bruno Dutertre and Leonardo de Moura},
  title = { The {Yices} {SMT} solver },
  year = {2006},
  documenturl = {http://yices.csl.sri.com/tool-paper.pdf},
  institution = { {SRI International} }
}
@techreport{SRI:simplex:dpllt,
  author = { Bruno Dutertre and Leonardo de Moura},
  title = { Integrating Simplex with {DPLL(T)} },
  year = {2006},
  institution = { {SRI International} },
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/sri-csl-06-01.pdf}
}
@inproceedings{dMR:SAT'2002,
  author = {Leonardo de Moura and
               Harald Rue{\ss}},
  title = { Lemmas on demand for satisfiability solvers },
  year = {2002},
  booktitle = {Symposium on the Theory and Applications of Satisfiability Testing (SAT'02),
                Cincinnati, USA},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/sat02.pdf}
}
@techreport{SRI:test:generation,
  author = { Gr{\'e}goire Hamon and  Leonardo de Moura and John Rushby},
  title = { Automated test generation with {SAL}},
  year = {2005},
  institution = { {SRI International} },
  note = { {CSL} Technical Note},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/salatg.pdf}
}
@techreport{demoura2007relevancy,
  title = {Relevancy propagation},
  author = {Leonardo de Moura and Nikolaj Bj{\o}rner},
  year = {2007},
  number = { {MSR-TR-2007-140} },
  institution = { {Microsoft Research} },
  documenturl = {http://research.microsoft.com/projects/z3/relevancy.pdf}
}
@inproceedings{Moura05integratingverification,
  author = {Leonardo de Moura and Sam Owre and Harald Rue{\ss} and John Rushby and Natarajan Shankar},
  title = {Integrating verification components},
  booktitle = {In Verified Software: Theories, Tools, Experiments},
  year = {2005},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/vstte.pdf}
}
@inproceedings{BjornerDeMoura2009,
  author = {Nikolaj Bj{\o}rner and Leonardo de Moura},
  title = {$Z3^{10}$: Applications, Enablers, Challenges and Directions},
  year = {2009},
  booktitle = {Sixth International Workshop on Constraints in Formal Verification Grenoble, France},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/cfv09.pdf}
}
@inproceedings{deMouraPassmore09,
  author = {Leonardo de Moura and Grant Olney Passmore},
  title = {On Locally Minimal Nullstellensatz Proofs},
  year = {2009},
  booktitle = {7th International Workshop on Satisfiability Modulo Theories, {SMT}, Montreal, Canada},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/SMT-09.pdf}
}
@techreport{deMouraPassmore09ext,
  author = {Leonardo de Moura and Grant Olney Passmore},
  title = {On Locally Minimal Nullstellensatz Proofs},
  year = {2009},
  institution = { {Microsoft Research} },
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/MSR-TR-2009-90.pdf},
  number = { {MSR-TR-2009-90} }
}
@inproceedings{PassmoreDeMoura09,
  author = {Grant Olney Passmore and Leonardo de Moura},
  title = {Universality of Polynomial Positivity and a Variant of {Hilbert's} 17th Problem},
  year = {2009},
  booktitle = { Automated Deduction: Decidability, Complexity, Tractability, {ADDCT'09}, Montreal, Canada},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/addct-09.pdf}
}
@inproceedings{LPAR:Join:08,
  author = { Nikolaj Bj{\o}rner and  Bruno Dutertre and Leonardo de Moura },
  title = {Accelerating Lemma Learning using Joins - {DPPL(Join)}},
  year = {2008},
  booktitle = { 15th International Conference on Logic for Programming Artificial Intelligence and Reasoning, {LPAR'08}},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/joins.pdf}
}
@article{Barrettetal2012JAR,
  author = {Clark Barrett and
               Morgan Deters and
               Leonardo de Moura and
               Albert Oliveras and
               Aaron Stump},
  year = {2012},
  title = { {6 Years of SMT-COMP} },
  journal = {Journal of Automated Reasoning},
  documenturl = {http://www.springerlink.com/content/t5302157331451k7/}
}
@inproceedings{BjornerDeMouraTillmann09,
  author = { Nikolaj Bj{\o}rner and  Leonardo de Moura and Nikolai Tillmann },
  title = { Satisfiability Modulo Bit-precise Theories for Program Exploration },
  year = {2008},
  booktitle = { Fifth International Workshop on Constraints in Formal Verification, ({CFV'08}), Sydney, Australia },
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/smbpex.pdf}
}
@misc{deMoura-etal:HCSS03,
  author = {Leonardo de Moura and Harald Rue{\ss} and John Rushby and Natarajan Shankar},
  title = {Embedded Deduction With {ICS}},
  booktitle = {National Security Agency's Third High Confidence Software and Systems Conference},
  year = {2003},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/hcss03.pdf}
}
@article{whd12,
  author = {Christoph Wintersteiger and Youssef Hamadi and Leonardo de Moura},
  title = {Efficiently solving quantified bit-vector formulas},
  journal = ,
  publisher = {Springer},
  url = {http://dx.doi.org/10.1007/s10703-012-0156-2},
  year = {2012},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/ufbv_journal.pdf}
}
@incollection{tractability,
  author = {Nikolaj Bj{\o}rner and Leonardo de Moura},
  booktitle = {Handbook of Tractability},
  title = ,
  publisher = {Cambridge University Press},
  editors = {Lucas Bordeaux and Youssef Hamadi and Pushmeet Kohli and Robert Mateescu},
  documenturl = { http://research.microsoft.com/en-us/um/people/leonardo/files/tractability.pdf},
  year = {2012}
}

This file was generated by bibtex2html 1.96.