Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Mansutti, Alessio https://www.dagstuhl.de/lipics License: Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-99418
URL:

Extending Propositional Separation Logic for Robustness Properties

pdf-format:


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
Seminar: 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