| Z3 Theorem Prover | |
|---|---|
 | |
| Original author | Microsoft Research |
| Developer | Microsoft |
| Initial release | 2012; 14 years ago (2012) |
| Stable release | |
| Written in | C++ |
| Operating system | Windows,FreeBSD,Linux (Debian,Ubuntu),macOS |
| Platform | IA-32,x86-64,WebAssembly,arm64 |
| Type | Theorem prover |
| License | MIT License |
| Website | github |
| Repository | |
Z3, also known as theZ3 Theorem Prover, is asatisfiability modulo theories (SMT) solver developed byMicrosoft.[2]
Z3 was developed in theResearch in Software Engineering (RiSE) group atMicrosoft Research Redmond and is targeted at solving problems that arise insoftware verification andprogram analysis. Z3 supports arithmetic, fixed-size bit-vectors, extensional arrays, datatypes, uninterpreted functions, andquantifiers. Its main applications areextended static checking, test case generation, andpredicate abstraction.[citation needed]
Z3 was open sourced in the beginning of 2015.[3] The source code is licensed underMIT License and hosted onGitHub.[4]The solver can be built usingVisual Studio, amakefile or usingCMake and runs onWindows,FreeBSD,Linux, andmacOS.
The default input format for Z3 isSMTLIB2.It also has officially supportedbindings for severalprogramming languages, includingC,C++,Python,.NET,Java, andOCaml.[5]
In this example propositional logic assertions are checked using functions to represent the propositions a and b. The following Z3 script checks to see if:
(declare-fun a () Bool)(declare-fun b () Bool)(assert (not (= (not (and a b)) (or (not a)(not b)))))(check-sat)
Result:
unsat
Note that the script asserts thenegation of the proposition of interest. Theunsat result means that the negated proposition is not satisfiable, thus proving the desired result (De Morgan's law).
The following script solves the two given equations, finding suitable values for the variables a and b:
(declare-const a Int)(declare-const b Int)(assert (= (+ a b) 20))(assert (= (+ a (* 2 b)) 10))(check-sat)(get-model)
Result:
sat(model (define-fun b () Int -10) (define-fun a () Int 30))
In 2015, Z3 received theProgramming Languages Software Award fromACMSIGPLAN.[6][7] In 2018, Z3 received theTest of Time Award from theEuropean Joint Conferences on Theory and Practice of Software (ETAPS).[8] Microsoft researchers Nikolaj Bjørner andLeonardo de Moura received the 2019Herbrand Award for Distinguished Contributions to Automated Reasoning in recognition of their work in advancing theorem proving with Z3.[9][10]
| Main projects |
| ||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| MSR Labs applied research |
| ||||||||||||||
