Bottom-Up Shape Analysis

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 are 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 [17] to represent program states. A key ingredient of our inference rules is a strong biabduction 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 ...

• Type: Conference
• Year: 2009
• Where: SAS
• Authors: Bhargav S. Gulavani, Supratik Chakraborty, Ganesan Ramalingam, Aditya V. Nori
• Keywords: Bottom-up Shape Analysis, Formal Methods, Hoare Triples, Inference Rules, SAS 2009