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 best transformers. In fact, algorithms are known for only a few abstract domains.

This paper presents a parametric framework that, for some abstract domains, is capable of obtaining best transformers in the limit. Because the method approaches best transformers from ``above'', if the computation takes too much time it can be stopped to yield a sound abstract transformer. Thus, the framework provides a tunable algorithm that offers a performance-versus-precision trade-off.

We describe instantiations of the framework for well-known abstract domains, such as intervals, polyhedra, and Cartesian predicate abstraction. We also show that the framework applies to several new variants of predicate-abstraction domains that we define in the paper.

(Click here to access the paper: PDF.)