A Method for Symbolic Computation of Abstract Operations
Aditya Thakur and Thomas Reps
In 1979, Cousot and Cousot gave a specification of the best (most-precise)
abstract transformer possible for a given concrete transformer and a given
abstract domain. Unfortunately, their specification does not lead to
an algorithm for obtaining the best transformer. In fact, algorithms are
known for only a few abstract domains.
This paper presents a parametric framework that, for a
given abstract domain A and logic L,
computes successively better A values that over-approximate
the set of states defined by an arbitrary formula in L.
Because the method approaches the most-precise A
value from ``above'', if it is taking too much time,
a safe answer can be returned at any time.
For certain combinations of A and L,
the framework is complete -- i.e., with enough resources,
it computes the most-precise abstract value possible.
(Click here to access the paper:
PDF.)
University of Wisconsin