A Relational Approach to Interprocedural Shape Analysis

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.

• Type: Conference
• Year: 2004
• Where: SAS
• Authors: Bertrand Jeannet, Alexey Loginov, Thomas W. Reps, Shmuel Sagiv
• Keywords: Formal Methods, Interprocedural Shape Analysis, Recursive Procedure Calls, SAS 2004, Settings—for Interprocedural Shape