Bilateral Algorithms for Symbolic Abstraction
Aditya Thakur, Matt Elder, and Thomas Reps
Given a concrete domain C, a concrete operation tau: C -> C, and an
abstract domain A, a fundamental problem in abstract interpretation is
to find the best abstract transformer tau#: A -> A that
over-approximates tau. This problem, as well as several other
operations needed by an abstract interpreter, can be reduced to the
problem of symbolic abstraction: the symbolic abstraction of a
formula phi in logic L, denoted by alphaHat(phi), is the best value in
A that over-approximates the meaning of phi. When the concrete
semantics of tau is defined in L using a formula psi that specifies
the relation between input and output states, the best abstract
transformer tau# can be computed as alphaHat(psi).
In this paper, we present a new framework for performing symbolic
abstraction, discuss its properties, and present several
instantiations for various logics and abstract domains. The key
innovation is to use a bilateral successive-approximation
algorithm, which maintains both an over-approximation and an
under-approximation of the desired answer.
(Click here to access the paper:
PDF;
(c) Springer-Verlag.)
University of Wisconsin