A Logical Model for Relational Abstract Domains

By: R. Giacobazzi and F. Scozzari

Roberto Giacobazzi
Dip. di Informatica
Univ. di Pisa
Corso Italia 40, 56125 Pisa (Italy)


In this paper we introduce the notion of Heyting completion in abstract interpretation, and we prove that it supplies, by means of intuitionistic implication, a logical basis to specify relational domains for program analyses and abstract interpretations. In particular we prove that Heyting completion provides a model for Cousot's reduced cardinal power of abstract domains. We introduce a uniform algebraic setting where complex abstract domains can be specified by simple logic formulas, or as solutions of recursive abstract domain equations, involving few basic operations for domain construction, all characterized by a clean logical interpretation. We apply our framework to characterize directionality and condensing in downward closed analysis of (constraint) logic programs. This paper is an extended version of Intuitionistic implication in abstract interpretation (PLILP'97, 1997).

Available: Not yet!

Related works by the authors:
  • A Unifying View on Abstract Domain Design (ACM Comp. Surveys 28(2):333-336, 1996)
  • The reduced relative power operation on abstract domains (Theor. Comp. Science, 1998)
  • Refining and compressing abstract domains (ICALP'97, 1997).

  • giaco@sci.univr.it