DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2017.25

On Symbolic Heaps Modulo Permission Theories

Authors: Stéphane Demri, Etienne Lozes, and Denis Lugiez

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

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.

Cite as

Stéphane Demri, Etienne Lozes, and Denis Lugiez. On Symbolic Heaps Modulo Permission Theories. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 25:1-25:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{demri_et_al:LIPIcs.FSTTCS.2017.25,
  author =	{Demri, St\'{e}phane and Lozes, Etienne and Lugiez, Denis},
  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 =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.25},
  URN =		{urn:nbn:de:0030-drops-83887},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.25},
  annote =	{Keywords: separation logic, entailment, permission, reasoning modulo theories}
}

Search Results

Documents authored by Lugiez, Denis

On Symbolic Heaps Modulo Permission Theories

Abstract

Cite as

Thanks for your feedback!

Could not send message