Strand: A logic combining heap structures and data

Strand ("STRucture ANd Data") is a logic that allows reasoning with heap-manipulating programs using deductive verification and SMT solvers. Strand formulas express constraints involving heap structures and the data they contain. Strand is powerful for it allows existential and universal quantification over the nodes and complex combinations of data constraints and structural constraints.

There is a powerful fragment of Strand for which satisfiability is decidable, where the decision procedure works by combining the theory of MSO over recursive data structures and the quantifier-free theory of the underlying data-logic.

Strand can be used to reason about the correctness of programs, in terms of verifying Hoare-triples where the pre- and post-conditions express both the structure of the heap as well as the data contained in them. The pre- and post-conditions allowed are Boolean combinations of pure existential or pure universal Strand formulas.

More details on Strand can be found here.


Experiments demonstrate the effectiveness and practicality of Strand by checking verification conditions generated in proving properties of several heap-manipulating programs, using a tool that combines an MSO decision procedure over trees (MONA) with an SMT solver for integer constraints (Z3).

Experimental results of program verification