1. Leonardo de Moura and Dejan Jovanović. A model-constructing satisfiability calculus. In 14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI, Rome, Italy, 2013, 2013. [ bib | .pdf ]
  2. Dejan Jovanović and Leonardo de Moura. Solving non-linear arithmetic. In Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, volume 7364 of Lecture Notes in Computer Science, pages 339-354. Springer, 2012. [ bib | .pdf ]
  3. Dejan Jovanović and Leonardo de Moura. Solving non-linear arithmetic. Technical Report MSR-TR-2012-20, Microsoft Research, 2012. [ bib | http ]
  4. Nikolaj Bjørner. Taking Satisfiability to the Next Level with Z3. IJCAR 2012.
  5. Anh-Dung Phan, Nikolaj Bjørner, David Monniaux. Anatomy of Alternating Quantifier Satisfiability. SMT workshop 2012. [.pdf ]
  6. Krystof Hoder and Nikolaj Bjørner. Generalized Property Directed Reachability. In SAT 2012. [.pdf ]
  7. Christoph Wintersteiger, Youssef Hamadi, and Leonardo de Moura. Efficiently solving quantified bit-vector formulas. Formal Methods in System Design, 2012. [ bib | http | .pdf ]
  8. Nikolaj Bjørner and Leonardo de Moura. Tractability and Modern Satisfiability Modulo Theories Solvers. In Handbook of Tractability. Cambridge University Press, 2012. [ bib | .pdf ]
  9. Krystof Hoder, Nikolaj Bjørner, and Leonardo de Moura. muZ - an efficient engine for fixed points with constraints. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 457-462, 2011. [ bib | .pdf ]
  10. Leonardo de Moura and Nikolaj Bjørner. Satisfiability modulo theories: introduction and applications. Commun. ACM, 54(9):69-77, 2011. [ bib | http ]
  11. Dejan Jovanović and Leonardo de Moura. Cutting to the chase solving linear integer arithmetic. In Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, volume 6803 of Lecture Notes in Computer Science, pages 338-353. Springer, 2011. [ bib | .pdf ]
  12. Maria Paola Bonacina, Christopher Lynch, and Leonardo de Moura. On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reasoning, 47(2):161-189, 2011. [ bib | .pdf ]
  13. Leonardo de Moura and Nikolaj Bjørner. Bugs, moles and skeletons: Symbolic reasoning for software development. In Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings, volume 6173 of Lecture Notes in Computer Science, pages 400-411. Springer, 2010. [ bib | .pdf ]
  14. Nikolaj Bjørner. Linear Quantifier Elimination as an Abstract Decision Procedure. IJCAR 2010.
  15. Margus Veanes, Nikolaj Bjørner, and Leonardo de Moura. Symbolic automata constraint solving. In Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings, volume 6397 of Lecture Notes in Computer Science, pages 640-654, 2010. [ bib | .pdf ]
  16. Ruzica Piskac, Leonardo de Moura, and Nikolaj Bjørner. Deciding effectively propositional logic using DPLL and substitution sets. J. Autom. Reasoning, 44(4):401-424, 2010. [ bib | http ]
  17. Christoph M. Wintersteiger, Youssef Hamadi, and Leonardo de Moura. Efficiently solving quantified bit-vector formulas. In Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23, pages 239-246. IEEE, 2010. [ bib | .pdf ]
  18. Leonardo de Moura and Nikolaj Bjørner. Generalized, efficient array decision procedures. In Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA, pages 45-52. IEEE, 2009. [ bib | .pdf ]
  19. Nikolaj Bjørner and Leonardo de Moura. Tapas: Theory combinations and practical applications. In Formal Modeling and Analysis of Timed Systems, 7th International Conference, FORMATS 2009, Budapest, Hungary, September 14-16, 2009. Proceedings, volume 5813 of Lecture Notes in Computer Science, pages 1-6. Springer, 2009. [ bib | http ]
  20. Leonardo de Moura and Nikolaj Bjørner. Satisfiability modulo theories: An appetizer. In Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009, Revised Selected Papers, volume 5902 of Lecture Notes in Computer Science, pages 23-36. Springer, 2009. [ bib | .pdf ] Nikolaj Bjørner and Joe Hendrix. Linear Functional Fixed-points. CAV 2009.
  21. Maria Paola Bonacina, Christopher Lynch, and Leonardo de Moura. On deciding satisfiability by DPLL(Γ+T) and unsound theorem proving. In Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, volume 5663 of Lecture Notes in Computer Science, pages 35-50. Springer, 2009. [ bib | .pdf ]
  22. Yeting Ge and Leonardo de Moura. Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science, pages 306-320. Springer, 2009. [ bib | .pdf ]
  23. Christoph M. Wintersteiger, Youssef Hamadi, and Leonardo de Moura. A concurrent portfolio approach to SMT solving. In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science, pages 715-720. Springer, 2009. [ bib | .pdf ]
  24. Grant Olney Passmore and Leonardo de Moura. Superfluous S-polynomials in strategy-independent groebner bases. In 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2009, Timisoara, Romania, September 26-29, 2009, pages 45-53. IEEE Computer Society, 2009. [ bib | .pdf ]
  25. Nikolaj Bjørner and Leonardo de Moura. z310: Applications, enablers, challenges and directions. In Sixth International Workshop on Constraints in Formal Verification Grenoble, France, 2009. [ bib | .pdf ]
  26. Leonardo de Moura and Grant Olney Passmore. On locally minimal nullstellensatz proofs. In 7th International Workshop on Satisfiability Modulo Theories, SMT, Montreal, Canada, 2009. [ bib | .pdf ]
  27. Leonardo de Moura and Grant Olney Passmore. On locally minimal nullstellensatz proofs. Technical Report MSR-TR-2009-90, Microsoft Research, 2009. [ bib | .pdf ]
  28. Grant Olney Passmore and Leonardo de Moura. Universality of polynomial positivity and a variant of Hilbert's 17th problem. In Automated Deduction: Decidability, Complexity, Tractability, ADDCT'09, Montreal, Canada, 2009. [ bib | .pdf ]
  29. Ruzica Piskac, Leonardo de Moura, and Nikolaj Bjørner. Deciding effectively propositional logic with equality. Technical Report MSR-TR-2008-181, Microsoft Research, 2008. [ bib | http ]
  30. Leonardo de Moura and Nikolaj Bjørner. Deciding effectively propositional logic using DPLL and substitution sets. In Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lecture Notes in Computer Science, pages 410-425. Springer, 2008. [ bib | .pdf ]
  31. Leonardo de Moura and Nikolaj Bjørner. Engineering DPLL(T) + Saturation. In Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lecture Notes in Computer Science, pages 475-490. Springer, 2008. [ bib | .pdf ]
  32. Leonardo de Moura and Nikolaj Bjørner. Proofs and refutations, and Z3. In 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, volume 418 of CEUR Workshop Proceedings. CEUR-WS.org, 2008. [ bib | .pdf ]
  33. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In 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, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. [ bib | .pdf ]
  34. Leonardo de Moura and Nikolaj Bjørner. Model-based theory combination. Electr. Notes Theor. Comput. Sci., 198(2):37-49, 2008. [ bib | .pdf ]
  35. Nikolaj Bjørner, Bruno Dutertre, and Leonardo de Moura. Accelerating lemma learning using joins - DPPL(Join). In 15th International Conference on Logic for Programming Artificial Intelligence and Reasoning, LPAR'08, 2008. [ bib | .pdf ]
  36. Nikolaj Bjørner, Leonardo de Moura, and Nikolai Tillmann. Satisfiability modulo bit-precise theories for program exploration. In Fifth International Workshop on Constraints in Formal Verification, (CFV'08), Sydney, Australia, 2008. [ bib | .pdf ]
  37. Leonardo de Moura and Nikolaj Bjørner. Efficient E-Matching for SMT solvers. In Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings, volume 4603 of Lecture Notes in Computer Science, pages 183-198. Springer, 2007. [ bib | .pdf ]

Last edited Dec 30, 2012 at 7:45 AM by leodemoura, version 3

Comments

No comments yet.