Dino Distefano
Queen Mary, University of London

Compositional Shape Analysis

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.

Host:  Peter Lee
Appointments: Diana Hyde <dhyde@andrew.cmu.edu>

Wednesday, July 2, 2008
3:30 p.m.
Wean Hall 8220

Principles of Programming Seminars