Building Complete Abstract Interpretations in a Linear Logic-based Setting

Abstract. Completeness is an important, but rather uncommon, prop-erty of abstract interpretations, ensuring that abstract computations are as precise as possible w.r.t. concrete ones. It turns out that completeness domains, and therefore it is an abstract domain property. Recently, the rst two authors proved that for a given abstract domain A, in all signif-icant cases, there exists the most abstract domain, called least complete extension of A, which includes A and induces a complete abstract in-terpretation. In addition to the standard formulation, we introduce and study a novel and particularly interesting type of completeness, called observation completeness. Standard and observation completeness are here considered in the context of quantales, i.e. models of linear logic, as concrete interpretations. In this setting, we prove that various kinds of least complete and observationally complete extensions exist and, more importantly, we show that such complete extensions can all be explicitly characterized by elegant linear logic-based formulations. As an applica-tion, we determine the least complete extension of a generic abstract do-main w.r.t. a standard bottom-up semantics for logic programs observing computed answer substitutions. This general result is then instantiated to the relevant case of groundness analysis.