Home	•	Docs	•	Download	•	Mail	•	FAQ	•	Awards	•	Status	•	MSR

An Efficient SMT Solver

Documentation

• FAQ (Frequently Asked Questions)
• Command line options
• INI parameters
• Z3 native input format
• SMT-LIB format
• Simplify input format
• Models
• C API
• C API examples
• Managed (.NET) API
• Managed (.NET) API examples
• OCaml API
• OCaml API examples

Publications

• 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.

Slides

• 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.
• 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.

Contributions

• Making use of F#'s math libraries together with Z3 (Many thanks to Byron Cook), F# source.
• Sudoku Solving using Z3 (Many thanks to Dmitry Ermolov).