Decidable entailments in separation logic with inductive definitions: beyond establishment

DOI10.4230/LIPICS.CSL.2021.20MaRDI QIDQ6839816zbMATH OpenFDO

Authors Mnacho Echenim, Radu Iosif, Nicolas Peltier

Publication date 23 March 2026

Copyright license Creative Commons Attribution 3.0 Unported

Full work available at URL https://doi.org/10.4230/LIPICS.CSL.2021.20

zbMATH Keywords

complexityentailmentsinduction definitionsinductive theorem provingseparation logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites work

• Beyond symbolic heaps: deciding separation logic with inductive definitions
• BI as an assertion language for mutable data structures
• Deciding entailments in inductive separation logic with tree automata
• Effective entailment checking for separation logic with inductive definitions
• Entailment checking in separation logic with inductive definitions is 2-ExpTime hard
• Foundations for decision problems in separation logic with general inductive predicates
• Graph minors. III. Planar tree-width
• Parametrized complexity theory.
• The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
• The tree width of separation logic with recursive definitions
• Unified reasoning about robustness properties of symbolic-heap separation logic

Cited in

(4)

• Deciding satisfiability for overlaid symbolic heaps
• Tractable and intractable entailment problems in separation logic with inductively defined predicates
• Expressiveness results for an inductive logic of separated relations
• A direct procedure to test entailment in a separation logic of relations

This page was built for publication: Decidable entailments in separation logic with inductive definitions: beyond establishment

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