An EXPTIME-complete entailment problem in separation logic

DOI10.1007/978-3-031-62687-6_11MaRDI QIDQ7034647zbMATH OpenFDO

Authors Nicolas Peltier

Publication date 31 January 2025

Full work available at URL https://doi.org/10.1007/978-3-031-62687-6_11

Mathematics Subject Classification ID

Logic in computer science (03B70) Analysis of algorithms and problem complexity (68Q25)

Cites work

• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
• A decision procedure for satisfiability in separation logic with inductive predicates
• A proof procedure for separation logic with inductive definitions and data
• An efficient cyclic entailment procedure in a fragment of separation logic
• Compositional entailment checking for a fragment of separation logic
• Deciding entailments in inductive separation logic with tree automata
• Entailment checking in separation logic with inductive definitions is 2-ExpTime hard
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• scientific article; zbMATH DE number 2081098 (Why is no real title available?)
• On automated lemma generation for separation logic with inductive definitions
• Separation logic with one quantified variable
• The Logic of Bunched Implications
• The tree width of separation logic with recursive definitions
• Tractability of separation logic with inductive definitions: beyond lists
• Tractable Reasoning in a Fragment of Separation Logic
• Unifying decidable entailments in separation logic with inductive definitions

Cited in

(1)

• The satisfiability problem in a separation logic of relations

This page was built for publication: An EXPTIME-complete entailment problem in separation logic

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