Sunday Tutorial, 15. November, 12:30 - 13:30
Bit-Precise Constraints:
Applications and Decision Procedures
Abstract
Satisfiability Modulo Theories (SMT) is about checking the satisfiability of logical formulas over one or more theories.
It draws on a combination of some of the most fundamental areas in computer science as it combines the problem of Boolean satisfiability with domains, such as, those studied in convex optimization and term-manipulating symbolic systems. It also draws on the most prolific problems in the past century of symbolic logic: the decision problem, completeness and incompleteness of logical theories, and finally complexity theory. The problem of modularly combining special purpose algorithms for each domain is as deep and intriguing as finding new algorithms that work particularly well in the context of a combination.
While the basis for SMT solvers is highly inspiring in the context of the intersection of logic, algorithms and systems, it is the role in software and hardware engineering applications that drives the field. Modern software, hardware analysis and model-based tools are increasingly complex and multi-faceted software systems. However, at their core is invariably a component using symbolic logic for describing states and transformations between them. SMT solvers are gaining a distinguished role in this context since they offer support for most domains encountered in programs. A well tuned SMT solver that takes into account the state-of-the-art breakthroughs usually scales orders of magnitude beyond custom ad-hoc solvers.
The solver Z3, developed at Microsoft Research, is a state-of-the-art SMT solver. It is largely a product of applications being pursued both in the context of research as well as in Microsoft's product groups.
This tutorial will take as starting point applications of Z3 where the bit-precise features are used. These applications include the Dynamic Symbolic Execution tools Pex, available externally for .NET developers, and SAGE, used internally for identifying security vulnerabilities in media format readers. Also included among consumers of bit-precise decision procedures is the model-based testing tool SpecExplorer, and the static program analysis tool PREfix that is used for analyzing Microsoft code repositories containing hundreds of millions lines of code. We give an introduction to decision procedures used (in Z3) for deciding bit-vector constraints and point to the challenges we have encountered for scaling bit-precise decision procedures.
Bio
Nikolaj Bjørner is a researcher and is currently managing the Foundations of Software Engineering (FSE) group at Microsoft Research in Redmond. FSE's research projects span logics for authentication (Yuri Gurevich), model program analysis (Margus Veanes), parameterized unit test case generation (Niklai Tillmann and Peli de Halleux), model-based design techniques (Ethan Jackson) and together with Leonardo de Moura work around the state-of-the-art Satisfiability Modulo Theories Solver Z3. Previously at Microsoft, Nikolaj developed and shipped the distributed file replication system (DFS-R) in quite different contexts such as Windows Server and Live Messenger, and in a more distant past he developed the Stanford Temporal Prover STeP.