{"id":614589,"date":"2019-10-16T08:00:12","date_gmt":"2019-10-16T15:00:12","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?p=614589"},"modified":"2019-10-23T16:28:28","modified_gmt":"2019-10-23T23:28:28","slug":"the-inner-magic-behind-the-z3-theorem-prover","status":"publish","type":"post","link":"https:\/\/www.microsoft.com\/en-us\/research\/blog\/the-inner-magic-behind-the-z3-theorem-prover\/","title":{"rendered":"The inner magic behind the Z3 theorem prover"},"content":{"rendered":"
\"Microsoft<\/a>

Microsoft researchers Nikolaj Bj\u00f8rner (left) and Leonardo de Moura (center) received the 2019 Herbrand Award for Distinguished Contributions to Automated Reasoning in recognition of their work in advancing theorem proving. They\u2019re pictured with Professor J\u00fcrgen Giesl (right) of the award committee.<\/p><\/div>\n

It\u2019s not uncommon for us to hear that the Z3 theorem prover is magical (opens in new tab)<\/span><\/a>, but the frequency of such complimentary feedback doesn\u2019t make it any less unexpected\u2014or humbling. When we began work on Z3 (opens in new tab)<\/span><\/a> in 2006, the design was motivated by two emerging use cases: program verification and dynamic symbolic execution. Research projects around program verification and dynamic symbolic execution, such as the verification-oriented programming language Dafny (opens in new tab)<\/span><\/a>, automatic test generation<\/a>, and fuzz testing<\/a>, had created an immense appetite for scalable and efficient solvers. While Z3, which is a satisfiability modulo theories (SMT) solver, was intentionally designed with a general interface that would allow easy incorporation into other types of software development and analysis tools, we couldn\u2019t possibly have dreamed up the kind of uses we\u2019ve seen (opens in new tab)<\/span><\/a>, from biological computation analysis<\/a> to solving pebbling games for quantum computers (opens in new tab)<\/span><\/a>.<\/p>\n

Z3 has more than 5,000 citations since 2008 (opens in new tab)<\/span><\/a> and has received numerous honors, including the 2018 Test of Time Award (opens in new tab)<\/span><\/a> from the European Joint Conferences on Theory & Practice of Software (ETAPS). In August, we were profoundly honored to receive the 2019 Herbrand Award for Distinguished Contributions to Automated Reasoning (opens in new tab)<\/span><\/a> in recognition of our work in advancing theorem proving. We attribute the software verification and SMT communities\u2019 embrace of Z3 to two valuable characteristics, its usability and scalability.<\/p>\n

Translating different language constructs into Z3 is easier than with theorem provers for pure first-order logic, as it offers one-to-one mapping from the data domain of the program being tested to the data domain of Z3, and it can handle larger, complex tasks often quickly. Saying it can significantly reduce wait time for results would be an understatement, as Microsoft Software Engineer Andrew Helwer (opens in new tab)<\/span><\/a> discovered. In sharing his experience working with Z3 to update Microsoft Azure firewalls (opens in new tab)<\/span><\/a>, a task he described as the thorniest technical problem he had encountered, he noted the theorem prover and constraint solver\u2014Z3 is capable of both checking whether a solution exists and, if so, providing one\u2014guaranteed the new firewalls offered the same high levels of security and availability as the old in less than a second. By Helwer\u2019s estimate, the same job would have taken a computer millions of years.<\/p>\n

This efficiency and raw power to crunch numbers and formulas is a result of what we consider to be the key insight that has allowed us to engineer the tool in several dimensions: a model-based approach to SMT solving.<\/p>\n

Model-based methods in Z3<\/h3>\n

SAT solving and first-order theorem proving have long been dominated by two methods, search and saturation. In search, you assign values one by one to variables and then backtrack when faced with contradictions. In saturation, you learn new facts from old facts. A paradigm shift occurred in SAT solvers when these two methods were combined using conflict-driven clause learning (opens in new tab)<\/span><\/a>. In a few steps, this new approach could eliminate entire classes of dead-ends that would require many more steps if they were enumerated explicitly, essentially making mistakes less costly. The development inspired us to explore executing the approach for infinite domains: How do you do it in the context of reasoning with integers, real numbers, or bit vectors?<\/p>\n

Understanding how to execute model-based methods in SMT solving began for us with the realization that the model being built during search could be used to explore far fewer cases when implementing the Nelson-Oppen combination method (opens in new tab)<\/span><\/a>: To combine results from two solvers, it\u2019s sufficient to reconcile only equalities that have to hold in the current candidate model. Consequently, the method is called model-based theory combination (opens in new tab)<\/span><\/a>. Instead of relying on elaborate mechanisms for extracting all possible equalities, the procedure asks the current candidate model for what equalities it assumes.<\/p>\n

This proved to be just an initial indication of several additional ways to exploit models. When solving formulas over arrays, Z3 uses the current candidate model to limit the number of times definitions for arrays are expanded and exposed to the search process. In a setting that generalizes the domain of arrays, when instantiating quantified formulas, Z3 uses the current candidate model to search for instances where the model is repaired to satisfy the quantifier in a method known as model-based quantifier instantiation (opens in new tab)<\/span><\/a>. Model-based techniques are also used to completely eliminate quantifiers over integers and reals; solve Horn clauses in the SPACER procedure<\/a>; and reason about integers and Tarski\u2019s logic of real numbers in standalone procedures. The idea even generalizes to a combination of other theories in the model-constructing satisfiability (mcSAT) procedure (opens in new tab)<\/span><\/a>. Every instance in which model-based techniques have been integrated in Z3 has led to increased speeds orders of magnitude greater than previous techniques. For Z3, model-based techniques are the difference-maker.<\/p>\n

Even though the high-level idea of using models is relatively straightforward, the machinery and sophistication that goes into using models for guiding saturation is substantial. To integrate them well requires turning the failed search branches into strong, irredundant search inferences. There is a deep connection between the process of creating these inferences and deducing a special form of Craig interpolants (opens in new tab)<\/span><\/a>. An inference that originates from a good interpolant eliminates not only the particular bad choice, but a maximal set of potential bad choices. A crucial part of engineering this integration is to ensure the interpolants contain enough information from the partial assignment still in play to separate it from extensions that are infeasible. The smarter and more efficiently you can compute interpolants, the better control you have over the search space.<\/p>\n

A robust SMT community<\/h3>\n

Carnegie Mellon University professor Jeremy Avigad (opens in new tab)<\/span><\/a>, in nominating Z3 for the SIGPLAN Programming Languages Software Award<\/a> it received in 2015, attributed the tool\u2019s seemingly \u201csupernatural abilities\u201d to \u201cextensive empirical research, supported by careful thought, clever insight, and a deep theoretical understanding.\u201d The award was presented to us and Christoph Wintersteiger<\/a>, from Microsoft Research Cambridge, who is a substantial contributor to Z3.<\/p>\n

Employing model-based techniques is<\/em> the clever insight, and it is the open standards created by the SMT community that has cultivated the empirical research essential to engineering quality tools. The Satisfiability Modulo Theories Library (SMT-LIB) initiative (opens in new tab)<\/span><\/a> and the TPTP Problem Library for Automated Theorem Proving (opens in new tab)<\/span><\/a> have without a doubt had a tremendous impact on advancing automated reasoning, allowing researchers to share benchmarks from their driving scenarios and their challenge problems.<\/p>\n

In its first 10-plus years, Z3 has surpassed our initial vision as a tool for program verification and dynamic symbolic execution thanks to the SMT community, and we look forward to what we hope will be many more advances, such as significantly more powerful arithmetical reasoning by our colleague Lev Nachmanson<\/a>, and many more use cases over the next 10 years. For more information on Z3 and details on variations of the model-based methods we\u2019ve taken with it, visit our publication page (opens in new tab)<\/span><\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"

It\u2019s not uncommon for us to hear that the Z3 theorem prover is magical, but the frequency of such complimentary feedback doesn\u2019t make it any less unexpected\u2014or humbling. When we began work on Z3 in 2006, the design was motivated by two emerging use cases: program verification and dynamic symbolic execution. Research projects around program […]<\/p>\n","protected":false},"author":39507,"featured_media":614619,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr-author-ordering":null,"msr_hide_image_in_river":0,"footnotes":""},"categories":[194488],"tags":[],"research-area":[13552,13546,13560,243138],"msr-region":[],"msr-event-type":[],"msr-locale":[268875],"msr-post-option":[],"msr-impact-theme":[],"msr-promo-type":[],"msr-podcast-series":[],"class_list":["post-614589","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-program-languages-and-software-engineering","msr-research-area-hardware-devices","msr-research-area-computational-sciences-mathematics","msr-research-area-programming-languages-software-engineering","msr-research-area-quantum","msr-locale-en_us"],"msr_event_details":{"start":"","end":"","location":""},"podcast_url":"","podcast_episode":"","msr_research_lab":[199565],"msr_impact_theme":[],"related-publications":[],"related-downloads":[],"related-videos":[],"related-academic-programs":[],"related-groups":[],"related-projects":[235367,169746,825511],"related-events":[],"related-researchers":[{"type":"edited_text","value":"Nikolaj Bj\u00f8rner","user_id":33067,"display_name":"Nikolaj Bj\u00f8rner","author_link":"Nikolaj Bj\u00f8rner<\/a>","is_active":false,"last_first":"Bj\u00f8rner, Nikolaj","people_section":0,"alias":"nbjorner"}],"msr_type":"Post","featured_image_thumbnail":"\"Microsoft","byline":"Nikolaj Bj\u00f8rner and Leonardo de Moura","formattedDate":"October 16, 2019","formattedExcerpt":"It\u2019s not uncommon for us to hear that the Z3 theorem prover is magical, but the frequency of such complimentary feedback doesn\u2019t make it any less unexpected\u2014or humbling. When we began work on Z3 in 2006, the design was motivated by two emerging use cases:…","locale":{"slug":"en_us","name":"English","native":"","english":"English"},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/614589","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/users\/39507"}],"replies":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/comments?post=614589"}],"version-history":[{"count":12,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/614589\/revisions"}],"predecessor-version":[{"id":617196,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/614589\/revisions\/617196"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/614619"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=614589"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/categories?post=614589"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/tags?post=614589"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=614589"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=614589"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=614589"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=614589"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=614589"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=614589"},{"taxonomy":"msr-promo-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-promo-type?post=614589"},{"taxonomy":"msr-podcast-series","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-podcast-series?post=614589"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}