Symbolic Abstraction: Algorithms and Applications

Abstract

This dissertation explores the use of abstraction in two areas of automated reasoning: verification of programs, and decision procedures for logics. Establishing that a program is correct is undecidable in general. Program-verification tools sidestep this tar-pit of undecidability by working on an abstraction of a program, which over-approximates the original program's behavior. The theory underlying this approach is called abstract interpretation. Developing a scalable and precise abstract interpreter is a challenging problem, especially when analyzing machine code. Abstraction provides a new language for the description of decision procedures, leading to new insights. I call such an abstraction-centric view of decision procedures Satisfiability Modulo Abstraction (SMA).

The unifying theme behind the dissertation is the concept of symbolic abstraction: Given a formula f in logic L and an abstract domain A, the symbolic abstraction of f is the strongest consequence of f expressible in A. This dissertation advances the field of abstract interpretation by presenting two new algorithms for performing symbolic abstraction, which can be used to synthesize various operations required by an abstract interpreter. The dissertation presents two new algorithms for computing inductive invariants for programs. The dissertation shows how the use of symbolic abstraction enables the design of a new abstract domain capable of representing bit-vector inequality invariants.

The dissertation advances the field of machine-code analysis by showing how symbolic abstraction can be used to implement machine-code analyses. Furthermore, the dissertation describes MCVETO, a new model-checking algorithm for machine code.

The dissertation advances the field of decision procedures by presenting a variety of SMA solvers. One is based on a generalization of Staalmarck's method, a decision procedure for propositional logic. When viewed through the lens of abstraction, Staalmarck's method can be lifted from propositional logic to richer logics, such as linear rational arithmetic. Furthermore, the SMA view shows that the generalized Staalmarck's method actually performs symbolic abstraction. Thus, the concept of symbolic abstraction brings forth the connection between abstract interpretation and decision procedures. The dissertation describes a new distributed decision procedure for propositional logic, called DiSSolve. Finally, the dissertation presents an SMA solver for a new fragment of separation logic.