Testing the satisfiability of formulas in separation logic with permissions

DOI10.1007/978-3-031-43513-3_23MaRDI QIDQ6541165zbMATH OpenFDO

Authors Nicolas Peltier

Publication date 17 May 2024

Copyright license Creative Commons Attribution 4.0 International

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A decision procedure for satisfiability in separation logic with inductive predicates
• BI as an assertion language for mutable data structures
• Compositional satisfiability solving in separation logic
• On Symbolic Heaps Modulo Permission Theories
• Permission accounting in separation logic
• Reasoning over permissions regions in concurrent separation logic
• Satisfiability of compositional separation logic with tree predicates and data constraints
• Separation logic modulo theories
• The Logic of Bunched Implications
• The tree width of separation logic with recursive definitions
• Unifying decidable entailments in separation logic with inductive definitions

This page was built for publication: Testing the satisfiability of formulas in separation logic with permissions

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