2011 | OriginalPaper | Chapter
Efficient Decision Procedures for Heaps Using STRAND
Authors : P. Madhusudan, Xiaokang Qiu
Published in: Static Analysis
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
The
Strand
[10] logic allows expressing structural properties of heaps combined with the data stored in the nodes of the heap. A semantic fragment of
Strand
as well as a syntactically defined subfragment of it are known to be decidable [10]. The known decision procedure works by combining a decision procedure for MSO on 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 known algorithm for deciding the syntactically defined decidable fragment (which is the same as the one for the semantically defined decidable fragment) involves solving large MSO formulas over trees, whose solution is the main bottleneck in obtaining efficient algorithms. In this paper, we focus on the syntactically defined decidable fragment of
Strand
, and obtain a new and more efficient algorithm. Using a set of experiments obtained from verification conditions of heap-manipulating programs, we show the practical benefits of the new algorithm.