Local Completeness in Abstract Interpretation

Completeness of an abstract interpretation is an ideal situation where the abstract interpreter is guaranteed to be compositional and producing no false alarm when used for verifying program correctness. Completeness for all possible programs and inputs is a very rare condition, met only by straightforward abstractions. In this paper we make a journey in the different forms of completeness in abstract interpretation that emerged in recent years. In particular, we consider the case of local completeness, requiring precision only on some specific, rather than all, program inputs. By leveraging this notion of local completeness, a logical proof system parameterized by an abstraction A, called LCLA, for Local Completeness Logic on A, has been put forward to prove or disprove program correctness. In this program logic a provable triple [p] c [q] not only ensures that all alarms raised for the post-condition q are true ones, but also that if q does not raise alarms then the program c cannot go wrong with the precondition p.