Dryad is a quantifier-free first-order logic over heaps augmented with recursive definitions of various types (e.g., an integer, a set/multiset of integers, etc.) defined for nodes that have a tree under them. While the first-order fragment gives the necessary power to talk precisely about nodes that are near neighbors, the recursive definitions allow expressing properties that require quantifiers, including reachability, collecting the set/multiset of keys in a tree, and defining natural metrics, like the height of a tree, that are typically useful in defining properties of trees.
A Hoare-triple corresponding to a basic path in a recursive imperative program with proof annotations written in a restricted sub-syntax of Dryad, can itself be expressed in Dryad. This leads to a systematic methodology for accurately unfolding the footprint on the heap uncovered by the program to find simple recursive proofs using abstraction and calls to SMT solvers.
More details on Dryad can be found in this paper:
Recursive Proofs for Inductive Tree Data-Structures