Z3, also known as the Z3 Theorem Prover, is a

satisfiability modulo theories In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involv ...

(SMT) solver developed by

Microsoft Microsoft Corporation is an American multinational corporation and technology company, technology conglomerate headquartered in Redmond, Washington. Founded in 1975, the company became influential in the History of personal computers#The ear ...

Overview

Z3 was developed in the ''Research in Software Engineering'' (RiSE) group at Microsoft Research Redmond and is targeted at solving problems that arise in

software verification Software verification is a discipline of software engineering, programming languages, and theory of computation whose goal is to assure that software satisfies the expected requirements. Broad scope and classification A broad definition of verif ...

and

program analysis In computer science, program analysis is the process of analyzing the behavior of computer programs regarding a property such as correctness, robustness, safety and liveness. Program analysis focuses on two major areas: program optimization an ...

. Z3 supports arithmetic, fixed-size bit-vectors, extensional arrays, datatypes, uninterpreted functions, and quantifiers. Its main applications are extended static checking, test case generation, and predicate abstraction. Z3 was open sourced in the beginning of 2015. The source code is licensed under

MIT License The MIT License is a permissive software license originating at the Massachusetts Institute of Technology (MIT) in the late 1980s. As a permissive license, it puts very few restrictions on reuse and therefore has high license compatibility. Unl ...

and hosted on

GitHub GitHub () is a Proprietary software, proprietary developer platform that allows developers to create, store, manage, and share their code. It uses Git to provide distributed version control and GitHub itself provides access control, bug trackin ...

. The solver can be built using

Visual Studio Visual Studio is an integrated development environment (IDE) developed by Microsoft. It is used to develop computer programs including web site, websites, web apps, web services and mobile apps. Visual Studio uses Microsoft software development ...

, a

makefile In software development, Make is a command-line interface software tool that performs actions ordered by configured Dependence analysis, dependencies as defined in a configuration file called a ''makefile''. It is commonly used for build automati ...

or using CMake and runs on

Windows Windows is a Product lining, product line of Proprietary software, proprietary graphical user interface, graphical operating systems developed and marketed by Microsoft. It is grouped into families and subfamilies that cater to particular sec ...

FreeBSD FreeBSD is a free-software Unix-like operating system descended from the Berkeley Software Distribution (BSD). The first version was released in 1993 developed from 386BSD, one of the first fully functional and free Unix clones on affordable ...

Linux Linux ( ) is a family of open source Unix-like operating systems based on the Linux kernel, an kernel (operating system), operating system kernel first released on September 17, 1991, by Linus Torvalds. Linux is typically package manager, pac ...

, and

macOS macOS, previously OS X and originally Mac OS X, is a Unix, Unix-based operating system developed and marketed by Apple Inc., Apple since 2001. It is the current operating system for Apple's Mac (computer), Mac computers. With ...

. The default input format for Z3 is SMTLIB2. It also has officially supported bindings for several

programming language A programming language is a system of notation for writing computer programs. Programming languages are described in terms of their Syntax (programming languages), syntax (form) and semantics (computer science), semantics (meaning), usually def ...

s, including C, C++, Python,

.NET The .NET platform (pronounced as "''dot net"'') is a free and open-source, managed code, managed computer software framework for Microsoft Windows, Windows, Linux, and macOS operating systems. The project is mainly developed by Microsoft emplo ...

Java Java is one of the Greater Sunda Islands in Indonesia. It is bordered by the Indian Ocean to the south and the Java Sea (a part of Pacific Ocean) to the north. With a population of 156.9 million people (including Madura) in mid 2024, proje ...

, and

OCaml OCaml ( , formerly Objective Caml) is a General-purpose programming language, general-purpose, High-level programming language, high-level, Comparison of multi-paradigm programming languages, multi-paradigm programming language which extends the ...

Examples

Propositional and predicate logic

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

\overline \equiv \overline \lor \overline

: (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 the ''negation'' of the proposition of interest. The ''unsat'' result means that the negated proposition is not satisfiable, thus proving the desired result (

De Morgan's law In propositional logic and Boolean algebra, De Morgan's laws, also known as De Morgan's theorem, are a pair of transformation rules that are both valid rules of inference. They are named after Augustus De Morgan, a 19th-century British mathemat ...

Solving equations

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) )

Awards

In 2015, Z3 received the ''Programming Languages Software Award'' from ACM

SIGPLAN SIGPLAN is the Association for Computing Machinery's Special Interest Group (SIG) on programming languages. This SIG explores programming language concepts and tools, focusing on design, implementation, practice, and theory. Its members are progra ...

. In 2018, Z3 received the ''Test of Time Award'' from the European Joint Conferences on Theory and Practice of Software (ETAPS). Microsoft researchers Nikolaj Bjørner and Leonardo de Moura received the 2019 Herbrand Award for Distinguished Contributions to Automated Reasoning in recognition of their work in advancing theorem proving with Z3.Herbrand Award
/ref>

References

External links

*
Official playground
{{Microsoft Research Free and open-source software Free software programmed in C++ Microsoft free software Microsoft Research Satisfiability modulo theories solvers Software using the MIT license 2012 software