Design of abstract domains using first-order logic

AbstractIn this paper we propose a simple framework based on first-order logic, for the design and decomposition of abstract domains for static analysis. An assertion language is chosen that specifies the properties of interest, and abstract domains on that assertion language are defined to be suitably chosen sets of assertions. Composition and decomposition of abstract domains is facilitated by their specification in assertion form. In particular, the operations of reduced product and disjunctive completion are formalized in this framework. Moreover, the notion of (conjunctive) factorization of sets of assertions is introduced, that allows one to decompose domains into ‘disjoint’ parts. We illustrate the use of this framework by studying typical abstract domains for ground-dependency and sharing analysis in logic programming