Queen Mary, University of London

Compositional Shape Analysis

Abstract:

In this talk we describe a compositional inter-procedural shape analysis, where each procedure is analyzed independently 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 proof 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.

Wednesday, July 2, 2008

3:30 p.m.

Wean Hall 8220

Principles
of Programming Seminars