The effects of adding reachability predicates in propositional separation logic

DOI10.1007/978-3-319-89366-2_26zbMATH Open1504.68128arXiv1810.05410OpenAlexW2796684949MaRDI QIDQ1653010FDOQ1653010

Authors: Alessio Mansutti, Stéphane Demri, Etienne Lozes 

Publication date: 17 July 2018

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.

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

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

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)

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
• Title not available (Why is that?)
• 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)