Sciweavers

Share
POPL
2009
ACM

Compositional shape analysis by means of bi-abduction

12 years 12 days ago
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...
Cristiano Calcagno, Dino Distefano, Peter W. O'Hea
Added 22 Nov 2009
Updated 22 Nov 2009
Type Conference
Year 2009
Where POPL
Authors Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
Comments (0)
books