##
Local Reasoning on Recursive Data Structures

Chu Duc Jiep and Joxan Jaffar
#### Abstract

We consider the problem of verifying programs which manipulate
recursive data structures. A main challenge here is how to perform
local reasoning so that the verification of subprograms, which operate
on different components of the data structure, can be combined.
Separation Logic (SL) was a significant advance in program
verification of data structures. It used a ``separating'' conjoin
operator in data structure specifications to construct heaps from
disjoint subheaps, and a ``frame rule'' to very elegantly realize
local reasoning. Consequently, when a program is verified in SL, the
proof is very natural and succinct. However, SL does not easily
accommodate \emph{shared} or \emph{cyclic} data structures.
In this paper, our new framework serves to maintain the essential
advantage, local reasoning, of SL. We begin with a domain of
discourse of explicit subheaps with recursive definitions. The
resulting specification language can describe arbitrary data
structures, and arbitrary sharing therein, thus enabling a very
precise specification of frames. The main contribution then is a
program verification method which combines strongest postcondition
reasoning in the form \emph{symbolic execution}, and \emph{unfolding
recursive definitions} of the data structure in question. Finally,
we present an implementation of our verifier, and demonstrate
automation on a number of representative programs. In particular, we
present the first automatic proof of a classic graph marking
algorithm, paving the way for dealing with a class of programs which
traverse a complex data structure.