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.

Z3banner

 

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

Z3icon

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.

 

Banner


Crazy Clocks
10/03/2024

It's that time again when the clocks change and  time is of the essence and I indulge my interest in crazy clocks. I am always surprised that there are still new ideas for how to display the time [ ... ]



The University of Tübingen's Self-Driving Cars Course
22/03/2024

The recorded lectures and the written material of a course on Self-Driving Cars at the University of Tübingen have been made available for free. It's a first class opportunity to learn the in an [ ... ]


More News

 

raspberry pi books

 

Comments




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

Last Updated ( Wednesday, 24 June 2015 )