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: https://drops.dagstuhl.de/opus/volltexte/2018/9941/
Mansutti, Alessio
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 |
