Completeness is an important, but rather uncommon, property of abstract interpretations, ensuring that abstract computations are as precise as possible w.r.t, concrete ones. It turns out that completeness for an abstract interpretation depends only on its underlying abstract domains, and therefore it is an abstract domain property. Recently, the first two authors proved that for a given abstract domain A, in all significant cases, there exists the most abstract domain, called least complete extension of A, which includes A and induces a complete abstract interpretation. 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 application, we determine the least complete extension of a generic abstract domain 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.

Building complete abstract interpretations in a linear logic-based setting

RANZATO, FRANCESCO;
1998

Abstract

Completeness is an important, but rather uncommon, property of abstract interpretations, ensuring that abstract computations are as precise as possible w.r.t, concrete ones. It turns out that completeness for an abstract interpretation depends only on its underlying abstract domains, and therefore it is an abstract domain property. Recently, the first two authors proved that for a given abstract domain A, in all significant cases, there exists the most abstract domain, called least complete extension of A, which includes A and induces a complete abstract interpretation. 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 application, we determine the least complete extension of a generic abstract domain 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.
Static Analysis, 5th International Symposium, SAS '98
3540650148
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11577/182287
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? 9
social impact