License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2017.25
URN: urn:nbn:de:0030-drops-83887
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/8388/
Go to the corresponding LIPIcs Volume Portal

Demri, Stéphane ; Lozes, Etienne ; Lugiez, Denis

On Symbolic Heaps Modulo Permission Theories

pdf-format:
LIPIcs-FSTTCS-2017-25.pdf (0.6 MB)

Abstract

We address the entailment problem for separation logic with symbolic heaps admitting list pred- icates and permissions for memory cells that are essential to express ownership of a heap region. In the permission-free case, the entailment problem is known to be in P. Herein, we design new decision procedures for solving the satisfiability and entailment problems that are parameterised by the permission theories. This permits the use of solvers dealing with the permission theory at hand, independently of the shape analysis. We also show that the entailment problem without list predicates is coNP-complete for several permission models, such as counting permissions and binary tree shares but the problem is in P for fractional permissions. Furthermore, when list predicates are added, we prove that the entailment problem is coNP-complete when the entail- ment problem for permission formulae is in coNP, assuming the write permission can be split into as many read permissions as desired. Finally, we show that the entailment problem for any Boolean permission model with infinite width is coNP-complete.

BibTeX - Entry

@InProceedings{demri_et_al:LIPIcs:2018:8388,
  author =	{St{\'e}phane Demri and Etienne Lozes and Denis Lugiez},
  title =	{{On Symbolic Heaps Modulo Permission Theories}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{25:1--25:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Satya Lokam and R. Ramanujam},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/8388},
  URN =		{urn:nbn:de:0030-drops-83887},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.25},
  annote =	{Keywords: separation logic, entailment, permission, reasoning modulo theories}
}

Keywords: separation logic, entailment, permission, reasoning modulo theories
Collection: 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)
Issue Date: 2018
Date of publication: 12.02.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI