ON THE POWER OF ABSTRACT INTERPRETATION

Increasingly sophisticated applications of static analysis make it important to precisely characterize the power of static analysis techniques. Sekar et al. recently studied the power of strictness analysis techniques and showed that strictness analysis is perfect up to variations in constants. We generalize this approach to abstract interpretation in general by defining a notion of similarity semantics. This semantics associates to a program a collection of interpretations all of which are obtained by blurring the distinctions that a particular static analysis ignores. We define completeness with respect to similarity semantics and obtain two completeness results. For first-order languages, abstract interpretation is complete with respect to a standard similarity semantics provided the base abstract domain is linearly ordered. For typed higher-order languages, it is complete with respect to logical similarity semantics again under the condition of linearly ordered base abstract domains.