On the Properties of Partial Completeness in Abstract Interpretation

We present a weakening of the completeness property in abstract interpretation. Completeness of a static analyzer represents the ideal situation where no false alarms are produced when answering queries on program behavior. Completeness, however, is a very rare condition to be satisfied in practice. We introduce the notion of partial completeness as a weakening of precision, namely, the abstract interpreter may produce a bounded number of false alarms, and then we show the key recursive properties of the class of programs for which an abstract interpreter is partially complete with a given bound of imprecision.