A Relational Approach to Interprocedural Shape Analysis

13 years 10 months ago

Download www.cs.wisc.edu

This paper addresses the veriﬁcation of properties of imperative programs with recursive procedure calls, heap-allocated storage, and destructive updating of pointer-valued ﬁelds—i.e., interprocedural shape analysis. It presents a way to harness some previously known approaches to interprocedural dataﬂow analysis—which in past work have been applied only to much less rich settings—for interprocedural shape analysis.

Bertrand Jeannet, Alexey Loginov, Thomas W. Reps,

Real-time Traffic

Formal Methods | Interprocedural Shape Analysis | Recursive Procedure Calls | SAS 2004 | Settings—for Interprocedural Shape |

claim paper

» Programming Paradigm Driven Heap Analysis

» On the Complexity of Function Pointer MayAlias Analysis

» Efficient ContextSensitive Shape Analysis with Graph Based Heap Models

» Regionbased shape analysis with tracked locations

» Error propagation analysis for file systems

» Global Medical Shape Analysis Using the LaplaceBeltrami Spectrum

» OffLine Signature Verification Recent Advances and Perspectives

» Conditional Variability of Statistical Shape Models Based on Surrogate Variables

Post Info
More Details (n/a)

Added	02 Jul 2010
Updated	02 Jul 2010
Type	Conference
Year	2004
Where	SAS
Authors	Bertrand Jeannet, Alexey Loginov, Thomas W. Reps, Shmuel Sagiv

Comments (0)

Sciweavers

A Relational Approach to Interprocedural Shape Analysis

Formal Methods | Interprocedural Shape Analysis | Recursive Procedure Calls | SAS 2004 | Settings—for Interprocedural Shape |

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers