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)

Rise4Fun

Getting Started with Z3: A Guide

#### Related Articles

Edit Distance Algorithm Is Optimal

Computational Complexity

Computability

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.

 Udacity's New Discovering Ethical AI Course12/04/2024Udacity has just launched an hour-long course on Ethical AI. Intended for a wide audience across many industries, it introduces to basic concepts and terms needed to step into the world of Ethica [ ... ] + Full Story We Built A Software Engineer20/03/2024One of the most worrying things about being a programmer today is the threat from AI. It has gone so far that NVIDA CEO Jensen Huang proclaims that you really shouldn't start training as a programmer  [ ... ] + Full Story More News

#### Comments

or email your comment to: comments@i-programmer.info

Last Updated ( Wednesday, 24 June 2015 )