Paper Info
Title
A relational approach to interprocedural shape analysis
Abstract
This article addresses the verification of properties of imperative programs with recursive procedure calls, heap-allocated storage, and destructive updating of pointer-valued fields, that is, interprocedural shape analysis. The article makes three contributions. — It introduces a new method for abstracting relations over memory configurations for use in abstract interpretation. — It shows how this method furnishes the elements needed for a compositional approach to shape analysis. In particular, abstracted relations are used to represent the shape transformation performed by a sequence of operations, and an overapproximation to relational composition can be performed using the meet operation of the domain of abstracted relations. — It applies these ideas in a new algorithm for context-sensitive interprocedural shape analysis. The algorithm creates procedure summaries using abstracted relations over memory configurations, and the meet-based composition operation provides a way to apply the summary transformer for a procedure P at each call site from which P is called. 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.
Year
DOI
Venue
2004
10.1145/1667048.1667050
ACM Transactions on Programming Languages and Systems (TOPLAS)
Keywords
DocType
Volume
destructive updating,recursive procedure call,abstract interpretation,abstracted relation,shape analysis,memory configuration,context-sensitive analysis,interprocedural shape analysis,new algorithm,shape transformation,relational approach,static analysis,recursive program,pointer analysis,interprocedural dataflow analysis,3-valued logic,procedure p,context-sensitive interprocedural shape analysis,procedure summary
Conference
32
Issue
ISSN
Citations 
2
0164-0925
28
PageRank 
References 
Authors
1.18
36
4
Name
Order
Citations
PageRank
Bertrand Jeannet164129.06
Alexey Loginov21578.35
Thomas W. Reps375251040.21
Mooly Sagiv43403236.93