%O Report %F jeannet04 %A Jeannet, B. %A Loginov, A. %A Reps, T. %A Sagiv, M. %T A relational approach to interprocedural shape analysis %N 0 %I University of Wisconsin-Madison %X 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 apply some previously known approaches to interprocedural dataflow analysis - which in past work have been applied only to a much less rich setting - so that they can be applied to programs that use heap-allocated storage and perform destructive updating %U http://www.cs.wisc.edu/wpis/abstracts/tr1505.abs.html %8 April %D 2004