Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
SAS04: Abstract for Paper 58
A Relational Approach to Interprocedural Shape Analysis
Bertrand Jeannet, Alexey Loginov, Thomas Reps, Mooly Sagiv
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.