Abstract Interpretations in the Framework of Invariant Sets

Abstract

We present a theory of abstract interpretations in the framework of invariant sets by translating the notions of lattices and Galois connections into this framework, and presenting their properties in terms of finitely supported objects. We introduce the notions of invariant correctness relation and invariant representation function, emphasize an equivalence between them, and establish the relationship between these notions and invariant Galois connections. Finally, we provide some widening and narrowing techniques in order to approximate the least fixed points of finitely supported transition functions.