Microsoft Z3 Theorem Prover Wins Award
Written by Kay Ewbank
Wednesday, 24 June 2015

Microsoft Research’s Z3 theorem prover has been awarded the 2015 ACM SIGPLAN Programming Languages Software Award.

The award is given for

“developing a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both.”

The announcement took place during PLDI 2015, the annual ACM SIGPLAN conference on Programming Language Design and Implementation. Z3 is an SMT solver.

SMT stands for Satisfiability Modulo Theories.

This is a complex idea, best explained in parts, starting with the ‘Theories’. Let’s suppose you have a theorem that you want to verify, where the logical formulas in the theorem can take multiple values. What you’d like is some automated way to show whether the theorem can be proved true by choosing particular values for the variables in your theorem, either finite or infinite values.

The more easily understandable applications might be integer arithmetic, or free functions. In practice such underlying theories are used on domain-specific models where theorem proving is required.

Examples might be finding out the conditions that have to be met for an application to use a particular code path; whether a code block is never going to be run; or whether some properties can be simultaneously true, thus indicating a bug.

So how can you satisfy the theory?

The brute force method would be to put together a truth table containing all the possible inputs that vary, with the resulting outcome, but anyone who’s done this for small numbers of variables knows how quickly the table becomes unmanageable.

What we usually want to know is whether a certain formula is ever true in the given theory.

This is what is known as satisfiability.

The Modulo part of the name means “under the presence of certain theories”.

Z3 is Microsoft’s implementation of an SMT solver – an automated alternative to let you show whether a theory can ever be satisfied. At Microsoft, developers have used Z3 to find security vulnerabilities.

They took over a billion constraints produced by Sage (Microsoft’s whitebox fuzzer, a technique for systematically identifying security vulnerabilities. The way Sage works is that an application is run with first inputs. Sage gathers constraints on inputs at conditional statements, then uses a constraint solver to generate new test inputs).

Microsoft says that Sage has saved the company millions of dollars that would have been spent fixing bugs in shipped products. Z3 also provides the basis for a cloud service security policy checker, the Pex test-case generation tool, a verifying C compiler and JavaScript malware detection, among others.

Z3 became open source under an MIT license in March. It supports Windows, OSX, Linux and FreeBSD, and since the code was released in October 2012, it has been downloaded more than 20,000 times. You can also call Z3 procedurally by using a variety of APIs available in C, C++, Java, .Net, OCaml and Python. You can try Z3 out in your own browser at Rise4Fun

Z3 Theorem Prover (GitHub)

Rise4Fun

Getting Started with Z3: A Guide

#### Related Articles

Edit Distance Algorithm Is Optimal

Computational Complexity

Computability

 AWS Training On Coursera, edX and Future Learn01/10/2020Amazon Web Services is running three versions of a new free training course on how to build modern Java apps on both Coursera and edX. + Full Story Lightstep Adds New GitHub Action22/10/2020Lightstep has announced a new GitHub action, Lightstep Pre-Deploy Check, designed to help developers be proactive about ensuring the quality and performance of their software before it’s actually de [ ... ] + Full Story More News