This paper addresses the verification of properties of imperative programs with recursive procedure calls, heap-allocated storage, and destructive updating of pointer-valued fields -- i.e., interprocedural shape analysis. It presents a way to harness some previously known approaches to interprocedural dataflow analysis -- which in past work have been applied only to much less rich settings -- for interprocedural shape analysis.

(Click here to access the paper: PostScript; PDF; (c) Springer-Verlag.)