Separation logic with linearly compositional inductive predicates and set data constraints
From MaRDI portal
Abstract: We identify difference-bound set constraints (DBS), an analogy of difference-bound arithmetic constraints for sets. DBS can express not only set constraints but also arithmetic constraints over set elements. We integrate DBS into separation logic with linearly compositional inductive predicates, obtaining a logic thereof where set data constraints of linear data structures can be specified. We show that the satisfiability of this logic is decidable. A crucial step of the decision procedure is to compute the transitive closure of DBS-definable set relations, to capture which we propose an extension of quantified set constraints with Presburger Arithmetic (RQSPA). The satisfiability of RQSPA is then shown to be decidable by harnessing advanced automata-theoretic techniques.
Recommendations
- A complete decision procedure for linearly compositional separation logic with data constraints
- Satisfiability of compositional separation logic with tree predicates and data constraints
- Compositional satisfiability solving in separation logic
- A decision procedure for satisfiability in separation logic with inductive predicates
- Foundations for decision problems in separation logic with general inductive predicates
- A proof procedure for separation logic with inductive definitions and data
- Tractability of separation logic with inductive definitions: beyond lists
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
- The SAT-based approach to separation logic
- A separation logic for a promising semantics
Cited in
(2)
This page was built for publication: Separation logic with linearly compositional inductive predicates and set data constraints
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2206230)
