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.CONCUR.2017.37
URN: urn:nbn:de:0030-drops-77826
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7782/
Go to the corresponding LIPIcs Volume Portal

Chen, Taolue ; Song, Fu ; Wu, Zhilin

Tractability of Separation Logic with Inductive Definitions: Beyond Lists

pdf-format:
LIPIcs-CONCUR-2017-37.pdf (0.7 MB)

Abstract

In 2011, Cook et al. showed that the satisfiability and entailment can be checked in polynomial time for a fragment of separation logic that allows for reasoning about programs with pointers and linked lists. In this paper, we investigate whether the tractability results can be extended to more expressive fragments of separation logic that allow defining data structures beyond linked lists. To this end, we introduce separation logic with a simply-nonlinear compositional inductive predicate where source, destination, and static parameters are identified explicitly (SLID[snc]). We show that if the inductive predicate has more than one source (destination) parameter, the satisfiability problem for SLID[snc] becomes intractable in general. This is exemplified by an inductive predicate for doubly linked list segments. By contrast, if the inductive predicate has only one source (destination) parameter, the satisfiability and entailment problems for SLID[snc] are tractable. In particular, the tractability results hold for inductive predicates that define list segments with tail pointers and trees with one hole.

BibTeX - Entry

@InProceedings{chen_et_al:LIPIcs:2017:7782,
  author =	{Taolue Chen and Fu Song and Zhilin Wu},
  title =	{{Tractability of Separation Logic with Inductive Definitions: Beyond Lists}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{37:1--37:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Roland Meyer and Uwe Nestmann},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7782},
  URN =		{urn:nbn:de:0030-drops-77826},
  doi =		{10.4230/LIPIcs.CONCUR.2017.37},
  annote =	{Keywords: Separation logic, Inductive definitions, Satisfiability, Entailment}
}

Keywords: Separation logic, Inductive definitions, Satisfiability, Entailment
Collection: 28th International Conference on Concurrency Theory (CONCUR 2017)
Issue Date: 2017
Date of publication: 01.09.2017

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