Dryad: Recursive proofs for inductive tree data-structures



Dryad is an extension of first-order logic with recursive definitions. Dryad supports the verification of full functional properties of inductive tree data-structures.

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
Under submission.

Experiments

Empirical evaluation shows that several complex tree data-structure algorithms can be checked against full functional specifications automatically, given pre- and post-conditions. We employ Z3, a state-of-the-art SMT solver, to check the generated verification conditions in the quantifier-free theory of integers and uninterpreted functions QF_UFLIA.

The experimental results are tabulated here.