Abstract Interpretation From a Denotational-semantics Perspective

Citations of this article
Mendeley users who have this article in their library.


The basic principles of abstract interpretation are explained in terms of Scott-Strachey-style denotational semantics: abstract-domain creation is defined as the selection of a finite approximant in the inverse-limit construction of a Scott-domain. Abstracted computation functions are defined in terms of an embedding-projection pair extracted from the inverse-limit construction. The key notions of abstract-interpretation backwards and forwards completeness are explained in terms of topologically closed and continuous maps in a coarsened version of the Scott-topology. Finally, the inductive-definition format of a language's denotational semantics is used as the framework into which the abstracted domain and abstracted computation functions are inserted, thus defining the language's abstract interpretation. © 2009 Elsevier B.V. All rights reserved.




Schmidt, D. A. (2009). Abstract Interpretation From a Denotational-semantics Perspective. Electronic Notes in Theoretical Computer Science, 249, 19–37. https://doi.org/10.1016/j.entcs.2009.07.082

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free