Completeness in abstract interpretation is an ideal and rare situation where the abstract semantics is able to take full advantage of the power of representation of the underlying abstract domain. In this paper, we develop an algebraic theory of completeness in abstract interpretation. We show that completeness is an abstract domain property and we prove that there always exist both the greatest complete restriction and the least complete extension of any abstract domain, with respect to continuous semantic functions. Under certain hypotheses, a constructive procedure for computing these complete domains is given. These methodologies provide advanced algebraic tools for manipulating abstract interpretations, which can be fruitfully used both in program analysis and in semantics design.

Completeness in abstract interpretation: a domain perspective

RANZATO, FRANCESCO
1997

Abstract

Completeness in abstract interpretation is an ideal and rare situation where the abstract semantics is able to take full advantage of the power of representation of the underlying abstract domain. In this paper, we develop an algebraic theory of completeness in abstract interpretation. We show that completeness is an abstract domain property and we prove that there always exist both the greatest complete restriction and the least complete extension of any abstract domain, with respect to continuous semantic functions. Under certain hypotheses, a constructive procedure for computing these complete domains is given. These methodologies provide advanced algebraic tools for manipulating abstract interpretations, which can be fruitfully used both in program analysis and in semantics design.
Algebraic Methodology and Software Technology, 6th International Conference, AMAST '97, Sydney, Australia
3540638881
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/182291
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 24
  • ???jsp.display-item.citation.isi??? ND
social impact