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.2018.42
URN: urn:nbn:de:0030-drops-99418
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9941/
Go to the corresponding LIPIcs Volume Portal

Mansutti, Alessio

Extending Propositional Separation Logic for Robustness Properties

pdf-format:
LIPIcs-FSTTCS-2018-42.pdf (0.7 MB)

Abstract

We study an extension of propositional separation logic that can specify robustness properties, such as acyclicity and garbage freedom, for automatic verification of stateful programs with singly-linked lists. We show that its satisfiability problem is PSpace-complete, whereas modest extensions of the logic are shown to be Tower-hard. As separating implication, reachability predicates (under some syntactical restrictions) and a unique quantified variable are allowed, this logic subsumes several PSpace-complete separation logics considered in previous works.

BibTeX - Entry

@InProceedings{mansutti:LIPIcs:2018:9941,
  author =	{Alessio Mansutti},
  title =	{{Extending Propositional Separation Logic for Robustness Properties}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software  Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{42:1--42:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Sumit Ganguly and Paritosh Pandya},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9941},
  URN =		{urn:nbn:de:0030-drops-99418},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.42},
  annote =	{Keywords: Separation logic, decision problems, reachability, logics on trees, interval temporal logic, adjuncts and quantifiers elimination}
}

Keywords: Separation logic, decision problems, reachability, logics on trees, interval temporal logic, adjuncts and quantifiers elimination
Collection: 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)
Issue Date: 2018
Date of publication: 05.12.2018

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