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. The paper makes three contributions:

The algorithm has been applied successfully to establish properties of both (i) recursive programs that manipulate lists, and (ii) recursive programs that manipulate binary trees.

(Click here to access the paper: PDF; (c) ACM.)