(Link)

Author: Leonardo de Moura (Microsoft Research) and Nikolaj Bjørner (Microsoft Research)

Reference: de Moura, Leonardo, and Nikolaj Bjørner. “Z3: An efficient SMT solver.” International conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008). Lecture Notes in Computer Science vol. 4963, 2008.

Why this paper? Cited by Shaking up the foundations of modern separation logic, Solvable Tuple Patterns and Their Applications to Program Verification, and Compositional Verification in Concurrent Separation Logic with Permissions Regions

The algorithm I use to supply reading for my blog (cited papers in recent articles as recommended to me by Google Scholar) sometimes sends me giant tomes, but this week I have the other extreme, at a mere four pages. This length, typical for tool demonstration papers at the conference TACAS, has not stopped this picking up 12,000 citations according to Google Scholar. Is this paper a remarkable gem, to pick up so many citations per page? Not exactly. Instead it is the tool that is the gem, with this paper that announces it merely the most convenient way to acknowledge its use.

Z3 is built on SAT solving, the process of automatically assigning Boolean truth values to propositional variables in a way that makes the formulae they appear in true (SATisfied). SAT is the ur-example of an NP-complete problem, as many other problems can be tractably encoded as SAT. While NP-complete problems are (barring a very surprising future proof of P = NP) intractable in general, there are so many useful examples that a huge amount of effort has been poured, with considerable success, into automation that works often enough to be useful. Satisfiability Modulo Theories (SMT) is the extension of SAT solving to cover some fragments of first order logic: in this case theories of linear arithmetic, bit-vectors, arrays, and tuples. This extension allows still more problems to be encoded and automatically attacked by an SMT solving tool like Z3. For example, all three of the papers that sent me to this paper use Z3 to look for solutions of encodings of correctness proofs of programs.