Efficient decision procedures for heaps using strand

P. Madhusudan, Xiaokang Qiu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 18th International Symposium, SAS 2011, Proceedings
Pages43-59
Number of pages17
DOIs
StatePublished - Sep 28 2011
Event18th International Static Analysis Symposium, SAS 2011 - Venice, Italy
Duration: Sep 14 2010Sep 16 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6887 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other18th International Static Analysis Symposium, SAS 2011
CountryItaly
CityVenice
Period9/14/109/16/10

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Efficient decision procedures for heaps using strand'. Together they form a unique fingerprint.

Cite this