Publications
cv-leonardo.bib
@article{doUnchained,
author = {Ullrich, Sebastian and de Moura, Leonardo},
title = {‘Do’ Unchained: Embracing Local Imperativity in a Purely Functional Language (Functional Pearl)},
year = {2022},
issue_date = {August 2022},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {6},
number = {ICFP},
url = {https://doi.org/10.1145/3547640},
doi = {10.1145/3547640},
journal = {Proc. ACM Program. Lang.},
month = {aug},
articleno = {109},
numpages = {28},
keywords = {Lean, functional programming, interactive theorem proving},
documenturl = {https://leanprover.github.io/papers/do.pdf}
}
@article{DBLP:journals/corr/abs-1802-03685,
author = {Daniel Selsam and
Matthew Lamm and
Benedikt B{\"{u}}nz and
Percy Liang and
Leonardo de Moura and
David L. Dill},
title = {Learning a {SAT} Solver from Single-Bit Supervision},
journal = {CoRR},
volume = {abs/1802.03685},
year = {2018},
url = {http://arxiv.org/abs/1802.03685},
archiveprefix = {arXiv},
eprint = {1802.03685},
timestamp = {Mon, 13 Aug 2018 16:47:15 +0200},
biburl = {https://dblp.org/rec/bib/journals/corr/abs-1802-03685},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/setss/BjornerMNW18,
author = {Nikolaj Bj{\o}rner and
Leonardo de Moura and
Lev Nachmanson and
Christoph M. Wintersteiger},
title = {Programming {Z3}},
booktitle = {Engineering Trustworthy Software Systems - 4th International School,
{SETSS} 2018, Chongqing, China, April 7-12, 2018, Tutorial Lectures},
pages = {148--201},
year = {2018},
url = {https://doi.org/10.1007/978-3-030-17601-3\_4},
doi = {10.1007/978-3-030-17601-3\_4},
timestamp = {Fri, 31 May 2019 09:51:39 +0200},
biburl = {https://dblp.org/rec/bib/conf/setss/BjornerMNW18},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{MetaProgLean,
author = {Gabriel Ebner and Sebastian Ullrich and Jared Roesch and Jeremy Avigad and Leonardo de Moura},
title = ,
journal = ,
issue_date = {September 2017},
volume = {1},
number = {ICFP},
month = aug,
year = {2017},
issn = {2475-1421},
pages = {34:1--34:29},
articleno = {34},
numpages = {29},
doi = {10.1145/3110278},
acmid = {3110278},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {dependent type theory, metaprogramming, tactic language, theorem proving},
documenturl = {https://leanprover.github.io/papers/tactic.pdf}
}
@inproceedings{10.1007/978-3-030-34175-6_13,
author = {Leijen, Daan
and Zorn, Benjamin
and de Moura, Leonardo},
editor = {Lin, Anthony Widjaja},
title = {Mimalloc: Free List Sharding in Action},
booktitle = {Programming Languages and Systems},
year = {2019},
publisher = {Springer International Publishing},
address = {Cham},
pages = {244--265},
isbn = {978-3-030-34175-6},
documenturl = {https://www.microsoft.com/en-us/research/uploads/prod/2019/06/mimalloc-tr-v1.pdf}
}
@inproceedings{10.1145/3453483.3454032,
author = {Reinking, Alex and Xie, Ningning and de Moura, Leonardo and Leijen, Daan},
title = {Perceus: Garbage Free Reference Counting with Reuse},
year = {2021},
isbn = {9781450383912},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3453483.3454032},
doi = {10.1145/3453483.3454032},
booktitle = {Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
pages = {96–111},
numpages = {16},
keywords = {Reference Counting, Handlers, Algebraic Effects},
location = {Virtual, Canada},
series = {PLDI 2021},
documenturl = {https://alexreinking.com/downloads/papers/perceus-garbage-free-reference-counting-with-reuse.pdf}
}
@misc{selsam2019learning,
title = {Learning a SAT Solver from Single-Bit Supervision},
author = {Daniel Selsam and Matthew Lamm and Benedikt Bünz and Percy Liang and Leonardo de Moura and David L. Dill},
year = {2019},
eprint = {1802.03685},
archiveprefix = {arXiv},
primaryclass = {cs.AI},
documenturl = {https://arxiv.org/pdf/1802.03685.pdf}
}
@inproceedings{UllrichdeMoura2019_1000120596,
author = {Ullrich, Sebastian and de Moura, Leonardo},
year = {2019},
title = {Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming [in press]},
eventtitle = {31st Symposium on Implementation and Application of Functional Languages},
eventtitleaddon = {IFL 2019},
eventdate = {2019-09-25/2019-09-27},
venue = {Singapur, Singapur},
booktitle = {31st Symposium on Implementation and Application of Functional Languages},
language = {english},
documenturl = {https://arxiv.org/pdf/1908.05647.pdf}
}
@inproceedings{10.1007/978-3-030-51054-1_10,
author = {Ullrich, Sebastian
and de Moura, Leonardo},
editor = {Peltier, Nicolas
and Sofronie-Stokkermans, Viorica},
title = {Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages},
booktitle = {Automated Reasoning},
year = {2020},
publisher = {Springer International Publishing},
address = {Cham},
pages = {167--182},
isbn = {978-3-030-51054-1},
documenturl = {https://arxiv.org/pdf/2001.10490.pdf}
}
@inproceedings{10.1007/978-3-030-79876-5_37,
author = {Moura, Leonardo de
and Ullrich, Sebastian},
editor = {Platzer, Andr{\'e}
and Sutcliffe, Geoff},
title = {The Lean 4 Theorem Prover and Programming Language},
booktitle = {Automated Deduction -- CADE 28},
year = {2021},
publisher = {Springer International Publishing},
address = {Cham},
pages = {625--635},
isbn = {978-3-030-79876-5},
documenturl = {https://leanprover.github.io/papers/lean4.pdf}
}
@misc{selsam2020tabled,
title = {Tabled Typeclass Resolution},
author = {Daniel Selsam and Sebastian Ullrich and Leonardo de Moura},
year = {2020},
eprint = {2001.04301},
archiveprefix = {arXiv},
primaryclass = {cs.PL},
documenturl = {https://arxiv.org/pdf/2001.04301.pdf}
}
@inproceedings{CCinITT,
author = {Daniel Selsam and Leonardo de Moura},
title = ,
booktitle = {Automated Reasoning, 8th International Joint Conference, University of Coimbra, Portugal},
year = {2016},
publisher = {Springer},
pages = {99--115},
isbn = {978-3-319-40229-1},
documenturl = {https://leanprover.github.io/papers/congr.pdf}
}
@inproceedings{fmcad14/RTdM,
author = {Andrew Reynolds and Cesare Tinelli and Leonardo de Moura},
title = ,
booktitle = {Proceedings of 14th International Conference on Formal Methods
in Computer-Aided Design, FMCAD 2014, 21-24 October 2014,
Lausanne, Switzerland},
year = {2014},
documenturl = {http://leodemoura.github.io/files/qcf.pdf}
}
@book{thprovinginlean,
author = {Jeremy Avigad and Leonardo de Moura and Soonho Kong},
title = ,
year = {2015},
documenturl = {http://leanprover.github.io/tutorial/tutorial.pdf}
}
@inproceedings{Lean,
author = {Leonardo de Moura and Soonho Kong and Jeremy Avigad and Floris van Doorn and Jakob von Raumer},
title = ,
year = {2015},
booktitle = {Automated Deduction - CADE-25, 25th International Conference
on Automated Deduction, Berlin, Germany, August 1-7, 2015,
Proceedings},
documenturl = {http://leodemoura.github.io/files/lean_cade25.pdf}
}
@misc{LeanCnstr,
author = {Leonardo de Moura and Jeremy Avigad and Soonho Kong and Cody Roux},
title = {Elaboration in Dependent Type Theory},
note = {Preprint, \url{http://arxiv.org/abs/1505.04324}},
year = {2015},
documenturl = {http://leodemoura.github.io/files/elaboration.pdf}
}
@inbook{BdMF15,
title = ,
author = {Clark Barrett and Leonardo de Moura and Pascal Fontaine},
booktitle = {All about Proofs, Proofs for All},
year = {2015},
series = {Mathematical Logic and Foundations},
editor = {David Delahaye and Bruno Woltzenlogel Paleo},
publisher = {College Publications},
address = {London, UK},
documenturl = {http://leodemoura.github.io/files/SMTProofs.pdf}
}
@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},
documenturl = {http://leodemoura.github.io/files/fmcad2013.pdf}
}
@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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/files/ematching.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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/files/cade09.pdf}
}
@inproceedings{DBLP:conf/cav/GeM09,
author = {Yeting Ge and
Leonardo de Moura},
title = {Complete Instantiation for Quantified Formulas in Satisfiability
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://leodemoura.github.io/files/ci.pdf}
}
@inproceedings{GeM09ext,
author = {Yeting Ge and
Leonardo de Moura},
title = {Complete Instantiation for Quantified Formulas in Satisfiability
Modulo Theories (extended version)},
year = {2009},
documenturl = { http://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/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://leodemoura.github.io/files/tractability.pdf},
year = {2012}
}
This file was generated by bibtex2html 1.99.
Leonardo de Moura
Senior Principal Applied Scientist in the Automated Reasoning Group at AWS
leodemoura0@gmail.com
