Shape Analysis with Inductive Recursion Synthesis [abstract] (ACM DL, PDF)
Bolei Guo, Neil Vachharajani, and David I. August
Proceedings of the ACM SIGPLAN 2007 Conference on
Programming Language Design and Implementation (PLDI), June 2007.
Accept Rate: 25% (45/178).
Separation logic with recursively defined predicates allows for
concise yet precise description of the shapes of data structures.
However, most uses of separation logic for program analysis rely on
pre-defined recursive predicates, limiting the class of programs
analyzable to those that manipulate only a priori data structures.
This paper describes a general algorithm based on \emph{inductive
program synthesis} that automatically infers recursive shape
invariants, yielding a shape analysis based on separation logic that
can be applied to any program. A key strength of separation logic is that it facilitates, via
explicit expression of structural separation, local reasoning
about heap where the effects of altering one part of a data structure
are analyzed in isolation from the rest. The interaction between
local reasoning and the global invariants given by recursive
predicates is a difficult area, especially in the presence of complex
internal sharing in the data structures. Existing approaches, using
logic rules specifically designed for the list predicate to unfold
and fold linked-lists, again require a priori knowledge about the
shapes of the data structures and do not easily generalize to more
complex data structures. We introduce a notion of ``truncation points"
in a recursive predicate, which gives rise to generic algorithms for
unfolding and folding arbitrary data structures.