Local Reasoning on Recursive Data Structures

Chu Duc Jiep and Joxan Jaffar


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.