Collecting operational abstract interpreters

The theory of abstract interpretation, introduced by Cousot and Cousot in 1977, is a general theory of the approximation of formal program semantics. It is a useful tool to prove the accuracy of static analysis and permits to express mathematically the link between the output of practical, approximate analysis and the original uncomputable program semantics. Given a programming language, abstract interpretation consists of giving several semantics linked by a relation of abstraction; a semantics is intended to be the mathematical characterization of a program’s possible behavior. There are several approaches to semantics each one focused on different properties of a given program. For instance, operational semantics focuses on how to execute a program, and in particular, structural operational semantics deals with how the single step of the computation takes place. On the other hand, the denotational approach is merely interested in the effect of the program’s computation, i.e., to find a relationship between input and output data passing through mathematical structures. It is clear that, since these two approaches are different, the final results must be coherent with each other, and this induces to speculate they may be considered equivalent in a suitable sense. Thanks to its streamlined notions and proofs, the denotational approach to abstract interpretation has already been studied many times, and many properties have been developed and well formalized. Instead, the operational correspondent versions have rarely been strictly formalized and proved, even if intuitively accepted as true. The main purpose of this work is to fill this gap: to study in detail the operational approach to abstract interpretation and to formalize in this particular setting some of the well-known denotational properties, providing mathematical proofs.