文章基本信息

标题：Tractability of Separation Logic with Inductive Definitions: Beyond Lists
本地全文：下载
作者：Taolue Chen ; Fu Song ; Zhilin Wu 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2017
卷号：85
页码：37:1-37:17
DOI：10.4230/LIPIcs.CONCUR.2017.37
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Separation logic; Inductive definitions; Satisfiability; Entailment