A Method for Symbolic Computation

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