Symbolic Implementation of the Best Transformer
Thomas Reps, Mooly Sagiv, and Greta Yorsh
This paper shows how to achieve, under certain conditions,
abstract-interpretation algorithms that enjoy the best possible
precision for a given abstraction.
The key idea is a simple process of successive approximation that
makes repeated calls to a decision procedure, and obtains the best
abstract value for a set of concrete stores that are represented
symbolically, using a logical formula.
(Click here to access the paper:
PostScript,
PDF.)