Inverse-limit and topological aspects of abstract interpretation

AbstractWe develop abstract-interpretation domain construction in terms of the inverse-limit construction of denotational semantics and topological principles: we define an abstract domain as a “structural approximation” of a concrete domain if the former exists as a finite approximant in the inverse-limit construction of the latter, and we extract the appropriate Galois connection for sound and complete abstract interpretations. The elements of the abstract domain denote (basic) open sets from the concrete domain’s Scott topology, and we hypothesize that every abstract domain, even non-structural approximations, defines a weakened form of topology on its corresponding concrete domain.We implement this observation by relaxing the definitions of topological open set and continuity; key results still hold. We show that families of closed and open sets defined by abstract domains generate post- and pre-condition analyses, respectively, and Giacobazzi’s forwards- and backwards-complete functions of abstract-interpretation theory are the topologically closed and continuous maps, respectively. Finally, we show that Smyth’s upper and lower topologies for power domains induce the overapproximating and underapproximating transition functions used for abstract-model checking