Inverse-limit and topological aspects of abstract interpretation (Q418811)

The paper develops abstract-interpretation domain construction in terms of the inverse-limit construction of denotational semantics and topological principles. The author defines 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 extracts 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 the author makes the hypothesis that every abstract domain, even non-structural approximations, defines a weakened form of topology on its corresponding concrete domain. This observation is implemented by relaxing the definitions of topological open set and continuity; key results still hold. It is showed 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, it is showed that Smyth's upper and lower topologies for power domains induce the overapproximating and underapproximating transition functions used for abstract-model checking.