Transforming Semantics by Abstract Interpretation
By: Roberto Giacobazzi and Isabella Mastroeni
Roberto
Giacobazzi
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
giaco@sci.univr.it
Isabella Mastroeni
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
mastroeni@sci.univr.it
Abstract:
In 1997, Cousot introduced a hierarchy where semantics are
related with each other by abstract interpretation. In this field we
consider the standard abstract domain transformers, devoted to refine
abstract domains in order to include attribute independent and
relational information, respectively the reduced product and power of
abstract domains, as domain operations to systematically design and
compare semantics by abstract interpretation. We first prove that
natural semantics can be decomposed in terms of complementary
attribute independent observables, leading to an algebraic
characterization of the symmetric structure of the
hierarchy. Moreover, we characterize some structural property of
semantics, such as their compositionality, in terms of simple abstract
domain equations.
This provides an equational presentation of most well-known semantics,
which is parametric on the observable and structural property of the
semantics, making it possible to systematically derive abstract
semantics, e.g. for program analysis, as solutions of abstract domain
equations.
Related papers:
mastroeni@sci.univr.it