@inproceedings{gulavani2009bottom-up,
author = {Gulavani, Bhargav and Chakraborty, Supratik and Ramalingam, G. and Nori, Aditya},
title = {Bottom-up Shape Analysis},
booktitle = {SAS '09: Static Analysis Symposium},
year = {2009},
month = {August},
abstract = {In this paper we present a new shape analysis algorithm. The key distinguishing aspect of our algorithm is that it is completely compositional, bottom­up and non­iterative. We present our algorithm as an inference system for computing Hoare triples summarizing heap manipulating programs. Our inference rules are compositional: Hoare triples for a compound statement is computed from the Hoare triples of its component statements. These inference rules are used as the basis for a bottom­-up shape analysis of programs. Specifically, we present a logic of iterated separation formula (LISF) which uses the iterated separating conjunct of Reynolds [16] to represent program states. A key ingredient of our inference rules is a strong bi­-abduction operation between two logical formulas. We describe sound strong bi­abduction and satisfiability decision procedures for LISF. We have built a prototype tool that implements these inference rules and have evaluated it on standard shape analysis benchmark programs. Pre­liminary results show that our tool can generate expressive summaries, which are complete functional specifications in many cases.},
publisher = {Springer Verlag},
url = {http://approjects.co.za/?big=en-us/research/publication/bottom-up-shape-analysis/},
edition = {SAS '09: Static Analysis Symposium},
}