Abstract Interpretations in the Framework of Invariant Sets

Article type: Research Article

Authors: Alexandru, Andrei | Ciobanu, Gabriel^*

Affiliations: Romanian Academy, Institute of Computer Science, Iaşi, Romania. andrei.alexandru@iit.academiaromana-is.ro; gabriel@info.uaic.ro

Correspondence: [*] Address for correspondence: Romanian Academy, Institute of Computer Science, Iaşi, Romania.

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.

Keywords: Invariant sets, finitely supported object, invariant Galois connection, abstract analysis

DOI: 10.3233/FI-2016-1321

Journal: Fundamenta Informaticae, vol. 144, no. 1, pp. 1-22, 2016