A Relational Approach to Interprocedural Shape Analysis
Bertrand Jeannet, Alexey Loginov, Thomas Reps, and Mooly Sagiv
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.)