Modular Shape Analysis for Dynamically Encapsulated Programs

In: Rocco De Nicolaed., 16th European Symposium on Programming (ESOP'07). LNCS, volume 4421, March, 2007

Authors

• Noam Rinetzky
• Arnd Poetzsch-Heffter
• Ganesan Ramalingam
• Mooly Sagiv
• Eran Yahav

Abstract

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.

BibTeX

@InProceedings{Rinetzky.Poetzsch-Heffter.EA07modular, 
   author = {Noam Rinetzky and Arnd Poetzsch-Heffter and Ganesan Ramalingam and Mooly Sagiv and Eran Yahav}
   title = {Modular Shape Analysis for Dynamically Encapsulated Programs},
   booktitle = {16th European Symposium on Programming (ESOP'07)},
   series = {LNCS},
   publisher = {Springer},
   month = {March},
   year = {2007},
}