Z3: an efficient SMT solver
- Leonardo de Moura ,
- Nikolaj Bjørner
2008 Tools and Algorithms for Construction and Analysis of Systems |
Published by Springer, Berlin, Heidelberg
Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.
Publication Downloads
Z3 automated theorem prover
May 31, 2018
Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license. Z3 can be built using Visual Studio, a Makefile or using CMake. It provides bindings for several programming languages including .NET, C, C++, Java, OCaml, Web Assembly and Python.