Compositional shape analysis by means of bi-abduction

This paper describes a compositional shape analysis, where each procedure is analyzed independently of its callers. The analysis uses an abstract domain based on a restricted fragment of separation logic, and assigns a collection of Hoare triples to each procedure; the triples provide an over-approximation of data structure usage. Compositionality brings its usual benefits ? increased potential to scale, ability to deal with unknown calling contexts, graceful way to deal with imprecision ? to shape analysis, for the first time. The analysis rests on a generalized form of abduction (inference of explanatory hypotheses) which we call bi-abduction. Biabduction displays abduction as a kind of inverse to the frame problem: it jointly infers anti-frames (missing portions of state) and frames (portions of state not touched by an operation), and is the basis of a new interprocedural analysis algorithm. We have implemented our analysis algorithm and we report case studies on smaller programs t...

• Type: Conference
• Year: 2009
• Where: POPL
• Authors: Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
• Keywords: Compositional Shape Analysis, Interprocedural Analysis Algorithm, Keywords Program Analysis, POPL 2009, Programming Languages