Shape analysis with inductive recursion synthesis

Bolei Guo, Neil Vachharajani, David I. August

Research output: Chapter in Book/Report/Conference proceedingConference contribution

44 Scopus citations

Abstract

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 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.

Original languageEnglish (US)
Title of host publicationPLDI'07
Subtitle of host publicationProceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation
Pages256-265
Number of pages10
DOIs
StatePublished - Oct 30 2007
EventPLDI'07: 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation - San Diego, CA, United States
Duration: Jun 10 2007Jun 13 2007

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Other

OtherPLDI'07: 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation
CountryUnited States
CitySan Diego, CA
Period6/10/076/13/07

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Artificial intelligence
  • Inductive recursion synthesis
  • Loop invariant inference
  • Separation logic
  • Shape analysis

Fingerprint Dive into the research topics of 'Shape analysis with inductive recursion synthesis'. Together they form a unique fingerprint.

  • Cite this

    Guo, B., Vachharajani, N., & August, D. I. (2007). Shape analysis with inductive recursion synthesis. In PLDI'07: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 256-265). (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)). https://doi.org/10.1145/1250734.1250764