Recent posts
Publications
cv-leonardo.bib
@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.97.
Leonardo de Moura
Principal Researcher in the RiSE group at
Microsoft Research
leonardo@microsoft.com
