Abstract domains for sharing analysis by optimal semantics

We propose a new technique for transforming abstract domains for logic program analysis in the theory of abstract interpretation. The basic idea is to exploit the notion of optimal semantics in order to improve the precision of a given analysis, with respect to a fixed property of interest. We show an application of our technique to the analysis of variable sharing. We propose a new domain for detecting pairs of independent variables which is obtained by transforming the Jacobs and Langen's domain for sharing analysis. The new domain has the advantage of being strictly more powerful than the original domain in detecting pair-sharing information and, at the same time, smaller in size.