Efficient Algorithms for Deciding Properties of Heaps using STRAND

In recent work [8], we defined a logic called Strand that expresses properties of heaps combined with the data stored in the nodes of the heap. The salient feature of this logic is that it can state complex properties of heaps with data, and also admits decidable fragments. We had identified both a semantic fragment of Strand, as well as a syntactic fragment of it that is decidable. The decision procedure worked by combining a decision procedure for trees (implemented by the tool Mona) and a decision procedure for the quantifier-free fragment of the data-theory (say, integers, and implemented using a solver like Z3). The decidability algorithm given for the syntactic decidable fragment used the same algorithm as the semantically decidable fragment, and involved solving large MSO formulas over trees, whose solution was the main bottleneck in obtaining efficient algorithms. In this paper, we focus on the syntactic decidable fragment of Strand, and obtain a new and more efficient algorithm. The new decision procedure also provides a simpler proof that this fragment of Strand is indeed decidable. This decision algorithm also has the remarkable feature that the constraint given to the decision procedure on trees is entirely independent of the Strand formula being checked, and depends only on the signature of the formula! This results in much smaller formulas that Mona can handle efficiently. Using a set of experiments obtained from verification conditions of heap-manipulating programs, we show the practical benefit of the new algorithm.