Recent Papers

---

• A Fast Linear-Arithmetic Solver for DPLL(T)
  by Bruno Dutertre, and Leonardo de Moura.
  Presented at CAV 06, Seattle, WA, 2006.
• Integrating Simplex with DPLL(T)
  by Bruno Dutertre, and Leonardo de Moura.
  CSL Technical Report SRI-CSL-06-01, March 2006.
• Design and Results of the 1st Satisfiability Modulo Theories Competition (SMT-COMP 2005)
  by Clark Barrett, Leonardo de Moura, and Aaron Stump.
  To be published in the Journal of Automated Reasoning (JAR).
• Integrating Verification Components
  by Leonardo de Moura, Sam Owre, Harald Rueß, John Rushby, and Natarajan Shankar.
  Invited position paper for Verified Software: Theories, Tools, Experiments, Zurich, Switzerland, October 2005.
• Automated Test Generation with SAL
  by Gregoire Hamon, Leonardo de Moura, and John Rushby.
  CSL Technical Note, January 2005.
• SMT-COMP: Satisfiability Modulo Theories Competition
  by Clark Barrett, Leonardo de Moura, and Aaron Stump.
  Presented at CAV 05, Edinburgh, Scotland, UK, 2005.
• Generating Efficient Test Sets with a Model Checker
  by Gregoire Hamon, Leonardo de Moura, and John Rushby.
  Presented at SEFM '04, Beijing, China, September 2004.
• Justifying Equality
  by Leonardo de Moura, Harald Rueß and Natarajan Shankar.
  Presented at PDPAR 2004, Cork, Ireland, July 2004.
• SAL 2
  by Leonardo de Moura, Sam Owre, Harald Rueß, John Rushby, N. Shankar, Maria Sorea, and Ashish Tiwari.
  In: Proceedings of Computer-Aided Verification, CAV '2004.
• An Experimental Evaluation of Ground Decision Procedures
  by Leonardo de Moura, and Harald Rueß.
  In: Proceedings of Computer-Aided Verification, CAV '2004.
• The ICS decision procedures for embedded deduction
  by Leonardo de Moura, Harald Rueß, Natarajan Shankar, and John Rushby.
  Presented at IJCAR 2004, Cork, Ireland, July 2004.
• From Simulation to Verification (and Back)
  by Harald Rueß, and Leonardo de Moura
  In: Proceedings of the 2003 Winter Simulation Conference, New Orleans, LA, December 2003, S. Chick, P.J. Sanchez, D. Ferrin, And D.J. Morrice (eds).
• Embedded Deduction with ICS
  by Leonardo de Moura, Harald Rueß, John Rushby, and Natarajan Shankar
  Presented at the third High Confidence Software and Systems Conference, Baltimore MD, April 2003.
• Bounded Model Checking and Induction: From Refutation to Verification
  by Leonardo de Moura, Harald Rueß, and Maria Sorea
  In: Proceedings of Computer-Aided Verification, CAV '2003.
• Lazy Theorem Proving for Bounded Model Checking over Infinite Domains
  by Leonardo de Moura, Harald Rueß, and Maria Sorea
  In: Proceedings of the 18th International Conference on Automated Deduction, CADE'2002.
• Lemmas on Demand for Satisfiability Solvers
  by Leonardo de Moura, and Harald Rueß
  In: Proceedings of Fifth International Symposium on the Theory and Applications of Satisfiability Testing, SAT'2002.

---

Leonardo de Moura: demoura@csl.sri.com