David I. August
Professor in the Department of Computer Science, Princeton University
Affiliated with the Department of Electrical Engineering, Princeton University
Ph.D. May 2000, Department of Electrical and Computer Engineering, University of Illinois at Urbana-Champaign

Office: Computer Science Building Room 221
Email: august@princeton.edu
Phone: (609) 258-2085
Fax: (609) 964-1699
Administrative Assistant: Pamela DelOrefice, (609) 258-5551

Front Page Publication List (with stats) Curriculum Vitae (PDF) The Liberty Research Group


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.