Optimality in goal-dependent Analysis of Sharing (full version)

In the context of abstract interpretation based static analysis, we cope with the problem of correctness and optimality for logic program analysis. We propose a new framework equipped with a denotational, goal-dependent semantics which refines many goal-driven frameworks appeared in the literature. The key point is the introduction of two specialized concrete operators for forward and backward unification. We prove that our goal-dependent semantics is correct w.r.t. computed answers and we provide the best correct approximations of all the operators involved in the semantics for set-sharing analysis. We show that the precision of the overall analysis is strictly improved and that, in some cases, we gain precision w.r.t. more complex domains involving linearity and freeness information.