Widening Operators for Abstract Interpretation

Abstract Interpretation, one of the most applied techniques for semantics based static analysis of software, is based on two main key-concepts: the correspondence between concrete and abstract semantics through Galois connections/insertions, and the feasibility of a fixed point computation of the abstract semantics, through the fast convergence of widening operators. The latter point is crucial to ensure the scalability of the analysis to large software systems. In this paper, we investigate which properties are necessary to support a systematic design of widening operators, by discussing and comparing different definitions in the literature, and by proposing various ways to combine them. In particular, we prove that, for Galois insertions, widening is preserved by abstraction, and we show how widening operators can be combined for the cartesian and reduced product of abstract domains.