2007 | OriginalPaper | Chapter
Modular Shape Analysis for Dynamically Encapsulated Programs
Authors : N. Rinetzky, A. Poetzsch-Heffter, G. Ramalingam, M. Sagiv, E. Yahav
Published in: Programming Languages and Systems
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We present a
modular
static analysis which identifies structural (shape) invariants for a subset of heap-manipulating programs. The subset is defined by means of a non-standard operational semantics which places certain restrictions on aliasing and sharing across modules. More specifically, we assume that live references (i.e., used before set) between subheaps manipulated by different modules form a tree. We develop a conservative static analysis algorithm by abstract interpretation of our non-standard semantics. Our
modular
algorithm also ensures that the program obeys the above mentioned restrictions.