An Efficient SMT Solver
- Z3^10: Applications, Enablers, Challenges and Directions, Nikolaj Bjørner, Leonardo de Moura, invited paper to CFV 2009.
- On deciding satisfiability by DPLL(Gamma+T) and unsound theorem proving, Maria Paola Bonacina, Christopher Lynch and Leonardo de Moura, CADE 2009.
- A Concurrent Portfolio Approach to SMT Solving, Christoph M. Wintersteiger, Youssef Hamadi and Leonardo de Moura, CAV 2009.
- Complete instantiation for quantified SMT formulas, Yeting Ge and Leonardo de Moura, CAV 2009.
- Linear Functional Fixed-points, Nikolaj Bjørner and Joe Hendrix CAV 2009.
- Accelerating lemma learning using joins - DPLL-Join, Nikolaj Bjørner, Bruno Dutetre, and Leonardo de Moura, Short paper at LPAR 2008.
- Proofs and Refutations and Z3, Leonardo de Moura and Nikolaj Bjørner. IWIL 2008
- Engineering DPLL(T) + Saturation, Leonardo de Moura and Nikolaj Bjørner, International Joint Conference on Automated Reasoning (IJCAR), Sydney, Australia, 2008.
- Deciding Effectively Propositional Logic using DPLL and substitution sets, Leonardo de Moura and Nikolaj Bjørner, International Joint Conference on Automated Reasoning (IJCAR), Sydney, Australia, 2008.
- Z3: An Efficient SMT Solver, Leonardo de Moura and Nikolaj Bjørner, Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Budapest, Hungary, 2008.
- Efficient E-matching for SMT solvers, Leonardo de Moura and Nikolaj Bjørner, Conference on Automated Deduction (CADE), Bremen, Germany, 2007.
- Model-based Theory Combination, Leonardo de Moura and Nikolaj Bjørner, Workshop on Satisfiability Modulo Theories (SMT), Berlin, Germany, 2007.
- Applications and Challenges in Satisfiability Modulo Theories, WING 2009, York, England (Powerpoint Slides).
- Quantifiers in Satisfiability Modulo Theories, Frontiers of Computational Reasoning, Cambridge, England (Powerpoint Slides).
- Quantifiers in Satisfiability Modulo Theories, Univeristy of Manchester, England (Powerpoint Slides).
- Accelerating lemma learning using joins, LPAR 2008, Doha, Qatar (Powerpoint Slides).
- Software Verification and Testing, NSF Workshop on Symbolic Computation for Constraint Satisfaction Problems, Virginia, 2008 (Powerpoint Slides).
- Invited Tutorial: Applications of SMT solvers in Software Verification, VSTTE'08, Toronto, Canada 2008 (Powerpoint Slides).
- Experiments in Software Verification using SMT solvers, VS Experiments'08, Toronto, Canada 2008 (Powerpoint Slides).
- Engineering DPLL(T) + Saturation (PDF), IJCAR'08, Sydney, Australia 2008 (Powerpoint Slides).
- Tutorial on SMT solvers in program analysis and Verification at Microsoft, Presented at IJCAR, Australia 2008; (PDF) (PowerPoint).
- SMT Solvers: Theory and Implementation, Summer School on Logic and Theorem Proving in Programming Languages, Oregon 2008.
- SMT Solvers in Program Verification and Analysis, MSR India Summer School on Programming Languages, Analysis and Verification, Bangalore, June 2008; Lecture 1 Lecture 2 Lecture 3 Lecture 4 Lecture 5 Lab Exercises; Student solutions: Ashish Sharma.
- SMT@Microsoft, Institute for Formal Models and Verification at the Johannes Kepler University in Linz, Austria 2008 (Powerpoint Slides).
- Z3: An Efficient SMT Solver, TACAS 2008 (Powerpoint Slides).
- Z3: An Efficient SMT Solver, McMaster University 2007.
- SMT@Microsoft, McMaster University 2007.
- SMT@Microsoft, AFM 2007.
- SMT@Microsoft, Intel 2007.
- Developing Efficient SMT Solvers, ESARLT 2007.
- SMT solvers: Introduction & Applications, Cambridge 2007.
- Z3: An Efficient SMT solver, MS Research Cambridge 2007.
- Efficient E-matching for SMT solvers, CADE 2007.
- Z3 0.1: An Efficient SMT solver, SMT-COMP 2007.
- Model-based Theory Combination, SMT 2007.
- Developing Efficient SMT Solvers, CMU 2007.
- Tutorial on SMT solvers, FMCAD 2006.
Last modified Fri Jun 19 21:10:00 2009