*Symbolic Abstraction: Algorithms and Applications*

Thakur, Aditya V.Computer Sciences Department, University of Wisconsin, Madison, 2014

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.

PDF@phdthesis{thakur_PHD14, author = {Thakur, Aditya V.}, title = {Symbolic Abstraction: Algorithms and Applications}, school = {Computer Sciences Department, University of Wisconsin, Madison}, type = {Ph.D. dissertation}, month = aug, year = {2014} }