{"id":507389,"date":"2018-10-02T09:58:25","date_gmt":"2018-10-02T16:58:25","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?p=507389"},"modified":"2018-10-03T08:44:28","modified_gmt":"2018-10-03T15:44:28","slug":"spacer-and-z3-accessible-reliable-model-checking-as-theorem-proving","status":"publish","type":"post","link":"https:\/\/www.microsoft.com\/en-us\/research\/blog\/spacer-and-z3-accessible-reliable-model-checking-as-theorem-proving\/","title":{"rendered":"SPACER and Z3: Accessible, reliable model checking as theorem proving"},"content":{"rendered":"

\"SPACER<\/p>\n

\u201cHow can one check a routine in the sense of making sure that it is right?\u201d asked Alan Turing in 1949, foreshadowing the science of program proving decades before it became a formally accepted field of computer science.<\/p>\n

Program proving, model checking, theorem solving \u2013 this is the terminology occupying the research space of computer science devoted to making sure programs work correctly. In the years since Turing theorized its necessity, the calculus of computation (also called computational logic) has grown into a large and dynamic field inextricably connected to real-world applications \u2013 and consequences \u2013 in artificial intelligence, constraint solving and the design and verification of both software and hardware systems. The kind of elusive mathematical logic that Turing alluded to is largely taken for granted today with ubiquitous tools that solve logical formulas used for modern program analysis. Theorem provers take the symbolic logic distilled by these tools and essentially deliver computer scientists the answer to Turing\u2019s question: Is it right?<\/em><\/p>\n

The highly-valued and tirelessly refined theorem provers are the essential instrument in this space and Z3 Theorem Prover from Microsoft Research, in creative interaction with academia, is the engine of choice. Z3 represents a long-running open source research project actively developed on GitHub (opens in new tab)<\/span><\/a> by top research talent from academia combined with Microsoft research and engineering muscle. It\u2019s made available under the MIT Open Source license and simply put is the leading solver for symbolic theorem proving in the world today.<\/p>\n

Z3 is a great example of what is possible with academic participation and long-term bets made by players like Microsoft Research in the solver community in terms of new applications and advances and myriad special-purpose features within the tool. One exciting such development is the SPACER solver in Z3. SPACER\u2019s origins go back to 2013 and Carnegie Mellon University where Arie Gurfinkel, currently Associate Professor of Computer Science at the University of Waterloo, in Ontario, Canada, and fellow graduate student Anvesh Komuravelli, now an engineer at Google, studied with Professor Edmund M. Clarke.<\/p>\n

\"Arie

Arie Gurfinkel<\/p><\/div>\n

Beyond Turing <\/strong><\/p>\n

What does SPACER accomplish, exactly?<\/p>\n

Alan Turing and later researchers developed methods for annotating computer programs with logical assertions that, when proved, would establish correctness properties. Some programs, such as device drivers that are a common albeit invisible part of daily life for users worldwide, can be automatically proved when their complex code is distilled into logical formulas known as constrained Horn clauses. SPACER specializes in solving Horn clauses. The use of Horn clause solving as a basis for automatic program proofs was ignited only a few years ago when Andrey Rybalchenko, now Principal Researcher at Microsoft Research Cambridge, established their use in a range of program proof applications.<\/p>\n

As a leading solver for constrained Horn clauses, SPACER integrates with end-to-end program verification systems. A great example is SeaHorn (opens in new tab)<\/span><\/a>, an open source tool on GitHub developed by Gurfinkel, a verification tool for C and C++ programs built on top of an LLVM framework. What enables SeaHorn to work is SPACER. What SeaHorn does is connect users of programming \u2013 as opposed to users of logic \u2013 with the verification tools, that is, analysis of programs. Safety checking of these programs is reduced to constrained Horn clauses that are then solved by SPACER. The Horn clause format, however, is not specifically tied to C programs or LLVM.<\/p>\n

\u201cThe Horn clause format provides a uniform logic-based framework for solving numerous fundamental problems in formal verification, including invariant inference, inter-procedural analysis, assume guarantee reasoning, and parameterized verification,\u201d said Sharon Shoham, a professor Tel Aviv University\u2019s School of Computer Science who actively uses SPACER.<\/p>\n

To be sure, SPACER is being applied in areas such as analysis of software defined networks, Blockchain contracts in IBM\u2019s Zeus system, ensuring that Blockchain contracts in fact reflect verifiable reality and that they cannot be broken by nefarious actors. Synthesizing quantum circuits is another use case in a hot topic, although this type of research is still in its infancy. Indeed, the applications out in the world that can target constrained Horn clauses is so rich that it is only a matter of time before analysis engines not yet using Horn clauses make the connection.<\/p>\n

SPACER\u2019s internals are equally fascinating, emphasized Nikolaj Bj\u00f8rner, Principal Researcher at Microsoft Research who\u2019d been looking into the same verification challenges for several years independently and who ultimately would work closely with Gurfinkel on Z3. SPACER builds on algorithms developed for symbolic model checking of finite-state machines and extends them for procedure calls and state machines over integers and other infinite data-types. How? \u201cIt draws on a very large set of sophisticated techniques developed in symbolic solving,\u201d explained Bj\u00f8rner. For example, SPACER exploits Farkas\u2019 lemma solvability theorem for linear programming duality to bound search for spurious counter-examples. It converts search over a stack machine into search over a simpler state machine by capturing techniques similar to Newton\u2019s iteration for finding roots. And it takes advantage of abstract interpretation methods and counter-example guided abstraction refinement to prune its search space. It gets better. \u201cMatteo Marescotti and Professor Natasha Sharygina, researchers at the University of Lugano have created a distributed version of SPACER to scale it even further,\u201d said Bj\u00f8rner. \u201cThese methods all integrate with an underlying solver that integrates the best of modern SAT search techniques.\u201d The Lugano researchers (opens in new tab)<\/span><\/a> use SPACER to scale up model checking to handle complex, real-world problems. An example is the parallelization of inductive reasoning for safety checking of programs.<\/p>\n

Interestingly, Gurfinkel\u2019s work on the Horn clause problem took as its starting point source code developed by Bj\u00f8rner, introducing significant innovations along the way. It began to appear that the approach of Gurfinkel and his students were pursuing would prove more fruitful and earlier this year the decision was taken to merge the two source codes, with SPACER becoming the main engine for constrained Horn clauses in Z3. \u201cIt\u2019s been four years of on-and-off interaction with Nikolaj, getting his insight but working separately on a code base and now getting it integrated in the Microsoft tool,\u201d said Gurfinkel.<\/p>\n

Z3, the system into which SPACER is now integrated, is very widely used in automated verification. Spacer represents new capability in Model Checking \u2013 that is, interaction in program verification. In 2007, the inventors of Model Checking were awarded the Turing Award. SPACER imports ideas from model checking into a theorem proving environment and conversely leverages advances in theorem proving to power model checking. This enables a lot of new applications, it makes it accessible to a lot of different users.<\/p>\n

Gurfinkel emphasized the immense significance accessibility has for users and he and his students having a delivery platform for their work. \u201cThere is a difference between building a prototype as an academic that doesn\u2019t leave your lab and getting what you\u2019ve built integrated into a product like Microsoft Research Z3, a much better engineered and developed system that users can rely on,\u201d said Gurfinkel.<\/p>\n

It echoed the opinions at Microsoft Research; SPACER functionality in Z3 represents significant value, both in providing additional services to its many users but as significantly, providing the technology in a package that is utterly accessible.<\/p>\n

And what would Turing think of SPACER in Z3, were it possible to show it to him? Gurfinkel paused and smiled before answering. \u201cI would hope that he would be impressed.\u201d<\/p>\n

\u201cHe did envision such tools and I think he would be at least very interested in seeing what we can actually do,\u201d he added.<\/p>\n","protected":false},"excerpt":{"rendered":"

\u201cHow can one check a routine in the sense of making sure that it is right?\u201d asked Alan Turing in 1949, foreshadowing the science of program proving decades before it became a formally accepted field of computer science. Program proving, model checking, theorem solving \u2013 this is the terminology occupying the research space of computer […]<\/p>\n","protected":false},"author":37583,"featured_media":507554,"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":"","footnotes":""},"categories":[194488],"tags":[],"research-area":[13546,13560],"msr-region":[],"msr-event-type":[],"msr-locale":[268875],"msr-post-option":[],"msr-impact-theme":[],"msr-promo-type":[],"msr-podcast-series":[],"class_list":["post-507389","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-program-languages-and-software-engineering","msr-research-area-computational-sciences-mathematics","msr-research-area-programming-languages-software-engineering","msr-locale-en_us"],"msr_event_details":{"start":"","end":"","location":""},"podcast_url":"","podcast_episode":"","msr_research_lab":[],"msr_impact_theme":[],"related-publications":[],"related-downloads":[],"related-videos":[],"related-academic-programs":[],"related-groups":[],"related-projects":[825511],"related-events":[],"related-researchers":[{"type":"user_nicename","value":"Nikolaj Bjorner","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":"\"SPACER","byline":"Nikolaj Bj\u00f8rner<\/a>","formattedDate":"October 2, 2018","formattedExcerpt":"\u201cHow can one check a routine in the sense of making sure that it is right?\u201d asked Alan Turing in 1949, foreshadowing the science of program proving decades before it became a formally accepted field of computer science. Program proving, model checking, theorem solving \u2013…","locale":{"slug":"en_us","name":"English","native":"","english":"English"},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/507389"}],"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\/37583"}],"replies":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/comments?post=507389"}],"version-history":[{"count":9,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/507389\/revisions"}],"predecessor-version":[{"id":508961,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/507389\/revisions\/508961"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/507554"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=507389"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/categories?post=507389"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/tags?post=507389"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=507389"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=507389"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=507389"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=507389"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=507389"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=507389"},{"taxonomy":"msr-promo-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-promo-type?post=507389"},{"taxonomy":"msr-podcast-series","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-podcast-series?post=507389"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}