CTL
15 septembre 2009 - 14h00
Compositional Shape Analysis by means of Bi-Abduction
par Dino Distefano de Queen Mary University, London
Abstract: This talk 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 (called bi-abduction) which is
the basis of a new interprocedural analysis algorithm.
We have implemented our analysis algorithm and we report case studies on
smaller programs to evaluate the quality of discovered specifications, and larger programs (e.g., an entire Linux distribution) to test scalability and graceful imprecision.
