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
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