  We face the problems of correctness, optimality and precision for the static
analysis of logic programs, using the theory of abstract interpretation. We
propose a framework with a denotational, goal-dependent semantics equipped with
two unification operators for forward unification (calling a procedure) and
backward unification (returning from a procedure). The latter is implemented
through a matching operation. Our proposal clarifies and unifies many different
frameworks and ideas on static analysis of logic programming in a single,
formal setting. On the abstract side, we focus on the domain Sharing by Jacobs
and Langen and provide the best correct approximation of all the primitive
semantic operators, namely, projection, renaming, forward and backward
unification. We show that the abstract unification operators are strictly more
precise than those in the literature defined over the same abstract domain. In
some cases, our operators are more precise than those developed for more
complex domains involving linearity and freeness.
  To appear in Theory and Practice of Logic Programming (TPLP)
