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.
论文与出版物下载
Z3 automated theorem prover
31 5 月, 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.