Transforming semantics by abstract interpretation (Q557807)

The most well-known structural properties of semantics, such as their precision, compositionality, and relation between complementary observables, by using standard abstract interpretation techniques are analyzed. It is proved that most of these properties can be characterized in terms of properties of the corresponding abstractions. This is achieved by isolating a suitable set of abstract domain transformers which allows one to design abstractions accordingly, providing a characterization of semantics of programming languages as solutions of simple abstract domain equations, involving both some basic observable property which has to be observed by the semantics and the abstract domain transformers necessary in order to achieve a suitable structural property.