Date and Time: Thursday, 4 September 2008, 15:30 - 16:30

Location: HG 6.96

Speaker: Dino Distefano (Royal Academy of Engineering, Logic and Semantics group, Queen Mary, University of London)

Title: Compositional Shape Analysis

Abstract:

In this talk I'll describe a compositional inter-procedural shape analysis, where each procedure is analyzed indepen dently of its callers. The analysis performs proof search in 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 interprocedural algorithm rests on a new form of abduction (inference of explanatory hypotheses), which is used in our analysis algorithm to discover preconditions by abductive inference of missing heap portions. We define a pr oof procedure for abduction, and use it to define our analysis algorithm.
We also report on the effects of the application of compositionality to a variety of large programs (up to >1 million LOC) by running experiments with an implementation of our algorithm.