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)
giaco@di.unipi.it
Abstract:
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:
giaco@sci.univr.it