Separation Logic with inductive predicate definitions (SL) and hyperedge replacement grammars (HRG) are established formalisms to describe the abstract shape of data structures maintained by heap manipulating programs. Fragments of both formalisms are known to coincide, and neither the entailment problem for SL nor its counterpart for HRGs, the inclusion problem, are decidable in general. We introduce tree-like grammars (TLG), a fragment of HRGs with a decidable inclusion problem. By the correspondence between HRGs and SL, we simultaneously obtain an equivalent SL fragment (SLtl) featuring some remarkable properties including a decidable entailment problem.
CITATION STYLE
Matheja, C., Jansen, C., & Noll, T. (2015). Tree-Like grammars and separation logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9458, pp. 90–108). Springer Verlag. https://doi.org/10.1007/978-3-319-26529-2_6
Mendeley helps you to discover research relevant for your work.