“How can one check a routine in the sense of making sure that it is right?” 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 – 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 – and consequences – 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’s question: Is it right?
Microsoft Research Podcast
AI Frontiers: Models and Systems with Ece Kamar
Ece Kamar explores short-term mitigation techniques to make these models viable components of the AI systems that give them purpose and shares the long-term research questions that will help maximize their value.
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) by top research talent from academia combined with Microsoft research and engineering muscle. It’s made available under the MIT Open Source license and simply put is the leading solver for symbolic theorem proving in the world today.
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’s 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.
Arie Gurfinkel
Beyond Turing
What does SPACER accomplish, exactly?
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.
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), 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 – as opposed to users of logic – 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.
“The 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,” said Sharon Shoham, a professor Tel Aviv University’s School of Computer Science who actively uses SPACER.
To be sure, SPACER is being applied in areas such as analysis of software defined networks, Blockchain contracts in IBM’s 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.
SPACER’s internals are equally fascinating, emphasized Nikolaj Bjørner, Principal Researcher at Microsoft Research who’d 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? “It draws on a very large set of sophisticated techniques developed in symbolic solving,” explained Bjørner. For example, SPACER exploits Farkas’ 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’s 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. “Matteo Marescotti and Professor Natasha Sharygina, researchers at the University of Lugano have created a distributed version of SPACER to scale it even further,” said Bjørner. “These methods all integrate with an underlying solver that integrates the best of modern SAT search techniques.” The Lugano researchers (opens in new tab) 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.
Interestingly, Gurfinkel’s work on the Horn clause problem took as its starting point source code developed by Bjørner, 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. “It’s 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,” said Gurfinkel.
Z3, the system into which SPACER is now integrated, is very widely used in automated verification. Spacer represents new capability in Model Checking – 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.
Gurfinkel emphasized the immense significance accessibility has for users and he and his students having a delivery platform for their work. “There is a difference between building a prototype as an academic that doesn’t leave your lab and getting what you’ve built integrated into a product like Microsoft Research Z3, a much better engineered and developed system that users can rely on,” said Gurfinkel.
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.
And what would Turing think of SPACER in Z3, were it possible to show it to him? Gurfinkel paused and smiled before answering. “I would hope that he would be impressed.”
“He did envision such tools and I think he would be at least very interested in seeing what we can actually do,” he added.
Mathematics 
Programming languages and software engineering