Legacy examples
The following examples are based on the old C API (Z3 3.x), but they can still be compiled with the new C API.
Online Tutorials
Slides
Introductory
- Z3: An Efficient SMT Solver (PDF), TACAS, Budapest, Hungary, 2008 (Powerpoint Slides).
- SMT@Microsoft, Max Planck Institut Informatik, Germany, 2009.
- Satisfiability Modulo Theories: An Appetizer, SBMF 2009, Gramado, Brazil (Powerpoint Slides)
Tutorials and Summer Schools
- First Summer School on Formal Techniques, Menlo Park, 2011.
- Satisfiability Modulo Theories (SMT): Ideas & Applications, Universita Degli Studi di Milano, Italy, March 2010 (part 1, part 2, part 3, part 4, assignment).
- Satisfiability with and without theories, Invited tutorial at KR'2010, Toronto, Canada, 2010
- On Designing and Implementing Satisfiability Modulo Theory Solvers, Summer School 2009: Verification Technology, Systems & Applications, Nancy, France (lecture 1, lecture 2)
- Invited Tutorial: Applications of SMT solvers in Software Verification, VSTTE'08, Toronto, Canada 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.
- Tutorial on SMT solvers, FMCAD 2006.
Technical presentations
- SMT: Techniques, Hurdles, Applications, First International SAT/SMT Solver Summer School 2011, MIT, 2011
- Orchestrating Decision Engines, CP'2011, Perugia, Italy, 2011
- Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development, Invited talk at IJCAR'2010, Edinburgh, UK, 2010
- Generalized and Efficient Array Decision Procedures, FMCAD, Austin TX, 2009.
- Applications and Challenges in Satisfiability Modulo Theories, WING 2009, York, England (Powerpoint Slides).
- Complete Instantiation for Quantified Formulas in SMT, CAV 2009, Grenoble, France (Powerpoint Slides).
- Quantifiers in Satisfiability Modulo Theories, Frontiers of Computational Reasoning, Cambridge, 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).
- 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).
- Efficient E-matching for SMT solvers, CADE 2007.
- Model-based Theory Combination, SMT 2007.
- Developing Efficient SMT Solvers, CMU 2007.
Publications
- Satisfiability Modulo Theories: Introduction and Applications, Leonardo de Moura and Nikolaj Bjorner, Communications of the ACM, 2011.
- Cutting to the Chase Solving Linear Integer Arithmetic, Dejan Jovanovic and Leonardo de Moura, CADE 2011.
- muZ: An Efficient Engine for Fixed Points with Constraints, Krystof Hoder, Nikolaj Bjorner, and Leonardo de Moura, CAV, 2011.
- Efficiently Solving Quantified Bit-Vector Formula, Christoph Wintersteiger, Youssef Hamadi and Leonardo de Moura, FMCAD 2010.
- Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development, Leonardo de Moura, Nikolaj Bjørner, IJCAR 2010.
- Linear Quantifier Elimination as an Abstract Decision Procedure., Nikolaj Bjørner, IJCAR 2010.
- Grobner Basis Construction Algorithms Based on Theorem Proving Saturation Loops, Grant Olney Passmore, Leonardo de Moura and Paul Jackson, Proceedings for "Decision Procedures in Software, Hardware and Bioware" Seminar at Dagstuhl, Germany, 2010.
- Generalized and Efficient Array Decision Procedures, Leonardo de Moura, Nikolaj Bjørner, FMCAD 2009.
- Satisfiability Modulo Theories: An Appetizer, Leonardo de Moura, Nikolaj Bjørner, invited paper to SBMF 2009.
- Superfluous S-polynomials in Strategy-Independent Grobner Bases, Grant Olney Passmore, Leonardo de Moura, 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), Timisoara, Romania, 2009.
- On Locally Minimal Nullstellensatz Proofs, Leonardo de Moura, Grant Olney Passmore, SMT 2009.
- 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.
