The effects of adding reachability predicates in propositional separation logic

DOI10.1007/978-3-319-89366-2_26MaRDI QIDQ1653010zbMATH OpenOpenAlexFDO

Authors Alessio Mansutti, Stéphane Demri, Etienne Lozes

Publication date 17 July 2018

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1810.05410

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Abstract: The list segment predicate ls used in separation logic for verifying programs with pointers is well-suited to express properties on singly-linked lists. We study the effects of adding ls to the full quantifier-free separation logic with the separating conjunction and implication, which is motivated by the recent design of new fragments in which all these ingredients are used indifferently and verification tools start to handle the magic wand connective. This is a very natural extension that has not been studied so far. We show that the restriction without the separating implication can be solved in polynomial space by using an appropriate abstraction for memory states whereas the full extension is shown undecidable by reduction from first-order separation logic. Many variants of the logic and fragments are also investigated from the computational point of view when ls is added, providing numerous results about adding reachability predicates to quantifier-free separation logic.

Recommendations

• Quantitative separation logic and programs with lists
• The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Quantitative Separation Logic and Programs with Lists
• Tractability of separation logic with inductive definitions: beyond lists

Cited in

(10)

• Foundations for entailment checking in quantitative separation logic
• Quantitative separation logic and programs with lists
• A complete axiomatisation for quantifier-free separation logic
• An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
• On temporal and separation logics
• scientific article; zbMATH DE number 7561347 (Why is no real title available?)
• Tractability of separation logic with inductive definitions: beyond lists
• An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
• Strong-separation logic
• Beyond Shapes: Lists with Ordered Data

This page was built for publication: The effects of adding reachability predicates in propositional separation logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1653010)