On Monday, June 15, Microsoft Research’s Z3 theorem prover received the 2015 ACM SIGPLAN Programming Languages Software Award (opens in new tab). 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 (opens in new tab), the annual ACM SIGPLAN conference on Programming Language Design and Implementation.
Z3’s lead developers—Nikolaj Bjorner (opens in new tab), Leonardo de Moura (opens in new tab) and Christoph Wintersteiger (opens in new tab), 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
GigaPath: Whole-Slide Foundation Model for Digital Pathology
Digital pathology helps decode tumor microenvironments for precision immunotherapy. In joint work with Providence and UW, we’re sharing Prov-GigaPath, the first whole-slide pathology foundation model, for advancing clinical research.
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 (opens in new tab).
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 (opens in new tab) and find out more on the project website (opens in new tab).
—Judith Bishop (opens in new tab), Director of Computer Science, Microsoft Research, Tom Ball (opens in new tab), Research Manager and Principal Researcher, Microsoft Research, and Ben Zorn (opens in new tab), Research Manager and Principal Researcher, Microsoft Research.
Learn more
Programming languages and software engineering