Symbolic Abstraction: Algorithms and Applications
Aditya V. Thakur
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 φ in logic L
and an abstract domain A,
the symbolic abstraction of φ is the strongest consequence
of φ 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 Stålmarck's method, a decision procedure for propositional
logic.
When viewed through the lens of abstraction, Stålmarck's
method can be lifted from propositional logic to richer logics, such
as linear rational arithmetic. Furthermore, the SMA view shows that
the generalized Stålmarck'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.
(Click here to access the dissertation:
PDF.)
University of Wisconsin