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.