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. © Springer-Verlag 2004.
CITATION STYLE
Jeannet, B., Loginov, A., Reps, T., & Sagiv, M. (2004). A relational approach to interprocedural shape analysis. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3148, 246–264. https://doi.org/10.1007/978-3-540-27864-1_19
Mendeley helps you to discover research relevant for your work.