Optimality in Goal-Dependent Analysis of Sharing

  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.