We consider the problem of computing the intersection (meet) of heap
abstractions, namely the common value of a set of abstract memory
stores.  This problem proves to have many applications in shape
analysis, such as interpreting program conditions, refining abstract
configurations, reasoning about procedures, and proving temporal
properties of heap-manipulating programs.  However, computing the meet
of heap abstractions is non-trivial; its definition as the least upper
bound of all lower bounds does not lead to an effective algorithm.
We show that the problem of computing meet is computationally hard.
We describe a constructive formulation of meet that is based on
finding certain relations between abstract heap objects. Enumerating
those relations is reduced to finding constrained matchings on
graphs.  We describe a prototype implementation of the algorithm for
proving temporal heap properties.  We applied the analysis to infer
rather precise compile-time garbage collection information on several
small but interesting Java programs, and obtained an empirical
evaluation of the meet algorithm.