Computer Sciences Dept.

A Relational Approach to Interprocedural Shape Analysis

Bertrand Jeannet, Alexey Loginov, Thomas Reps, 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 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.

Download this report (PDF)

Return to tech report index

Computer Science | UW Home