Microsoft Research Blog

The Microsoft Research blog provides in-depth views and perspectives from our researchers, scientists and engineers, plus information about noteworthy events and conferences, scholarships, and fellowships designed for academic and scientific communities.

Z3 wins 2015 ACM SIGPLAN Award

June 16, 2015 | By Microsoft blog editor

On Monday, June 15, Microsoft Research’s Z3 theorem prover received the 2015 ACM SIGPLAN Programming Languages Software Award. This prestigious award honors an institution or individuals 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’s lead developers—Nikolaj Bjorner, Leonardo de Moura and Christoph Wintersteiger, all of Microsoft Research—were cited for creating a highly efficient theorem prover and tool in the SMT (Satisfiability Modulo Theories) class.

Derek Dreyer, Chair of the Awards Committee, presents the Award to Christoph Wintersteiger, Leonardo de Moura and Nikolai Bjorner

Derek Dreyer, Chair of the Awards Committee, presents the award to Christoph Wintersteiger,

Leonardo de Moura, and Nikolai Bjorner

Z3 is a state-of-the art theorem prover that integrates specialized solvers for domains that are of relevance for program analysis, testing and verification. Z3 is a compelling integral component of such tools because these tools rely on reasoning about program states and transformations between states. 

At Microsoft, developers have used Z3 to solve more than a billion constraints produced by Sage, the world’s first whitebox fuzzer for finding security vulnerabilities. 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. Moreover, Z3’s powerful and versatile technology has inspired an entire generation of practical tools, including Spec#, Dafny, VCC, Havoc, Boogie, Slam, Yogi, Hyper-V, Spec Explorer and Terminator, which can been tested out on Rise4Fun.

Many years in the making, Z3 now supports all major platforms (Windows, OSX, Linux and FreeBSD). Since the code was released in October 2012, Z3 has been downloaded more than 20,000 times. Users can also call Z3 procedurally by using a variety of APIs available in C, C++, Java, .Net, OCaml and Python. Z3 became open source under an MIT license in March 2015.

With this release, Z3 has been adopted by an appreciative user community in a variety of tools for a wide range of uses, including general problem-solving, scheduling, optimization and software analysis. Being open source has definitely accelerated the development of the power of the system, in particular by accumulating contributions from the academic world, including theorists, tool-builders and users, for the benefit of all. Examples of tools in static analysis, verification and inference are Verifast, ScalaZ3, Why3, MetiTarski, SBV and ESC/Java2

In the academic world, Z3 has spawned more than 30 technical publications and more than 2,200 citations. It also provides an important tool for introducing students to SMT and theorem proving.

So congratulations to the Z3 team for this well-deserved recognition. You can try Z3 out in your own browser at Rise4Fun and find out more on the project website.

Judith Bishop, Director of Computer Science, Microsoft Research, Tom Ball, Research Manager and Principal Researcher, Microsoft Research, and Ben Zorn, Research Manager and Principal Researcher, Microsoft Research

Learn more