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 are powerful fragments 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 in this paper:
Decidable Logics Combining Heap Structures and Data (Slides)
by P. Madhusudan, Gennaro Parlato and Xiaokang Qiu.
38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL),
Austin, TX, 2011.
For a syntactic decidable fragment of Strand, there is a more efficient decision procedure. This decision procedure has the remarkable feature that the complexity of the decision procedure is entirely independent of the Strand formula being checked, and depends only on the signature of the formula! More details on this decision procedure can be found in this paper:
Efficient Decision Procedures for Heaps using STRAND (Slides)
by P. Madhusudan and Xiaokang Qiu.
18th International Static Analysis Symposium (SAS),
Venice, Italy, 2011.