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


More Information

Z3 Theorem Prover (GitHub)


Getting Started with Z3: A Guide

Related Articles

Edit Distance Algorithm Is Optimal       

Computational Complexity



To be informed about new articles on I Programmer, install the I Programmer Toolbar, subscribe to the RSS feed, follow us on, Twitter, FacebookGoogle+ or Linkedin,  or sign up for our weekly newsletter.



The State Of Secure Software Development - Three OpenSSF Courses

The Open Source Security Foundation has recently launched three brand new and free courses on Secure Software Development, which are hosted on edX.

Amazon Luna Goes Live

Amazon has launched Luna, a cloud gaming service that it says game developers can use to reach multiple endpoints from a single source.

More News






or email your comment to:

Last Updated ( Wednesday, 24 June 2015 )