文章基本信息

标题：Extending Propositional Separation Logic for Robustness Properties
本地全文：下载
作者：Alessio Mansutti
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：122
页码：1-23
DOI：10.4230/LIPIcs.FSTTCS.2018.42
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Separation logic; decision problems; reachability; logics on trees; interval temporal logic; adjuncts and quantifiers elimination