Shape analysis with inductive recursion synthesis

Bolei Guo, Neil Vachharajani, David I. August

Research output: Contribution to journalArticlepeer-review

17 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)
Pages (from-to)256-265
Number of pages10
JournalACM SIGPLAN Notices
Volume42
Issue number6
DOIs
StatePublished - Jun 2007

All Science Journal Classification (ASJC) codes

  • General Computer Science

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