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

Comments

Make a Comment or View Existing Comments Using Disqus

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