A Relational Approach to Interprocedural Shape Analysis
Show full item record
File(s):
- Author(s)
-
Jeannet, Bertrand; Loginov, Alexey; Reps, Thomas; Sagiv, Mooly
- Publisher
- University of Wisconsin-Madison Department of Computer Sciences
- Date
- Mar 15, 2012
- Abstract
- 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.
- Permanent link
-
http://digital.library.wisc.edu/1793/60398
- Export
-
Export to RefWorks
Part of
Show full item record