2026-07-20T11:57:06Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9941 2024-03-06T10:45:09Z ddc:004 open_access

Extending Propositional Separation Logic for Robustness Properties Mansutti, Alessio Separation logic decision problems reachability logics on trees interval temporal logic adjuncts and quantifiers elimination 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alessio Mansutti 2018 Is Part Of LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2018.42 urn:nbn:de:0030-drops-99418 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.42 eng https://creativecommons.org/licenses/by/3.0/legalcode