Testing the satisfiability of formulas in separation logic with permissions

DOI10.1007/978-3-031-43513-3_23MaRDI QIDQ6541165FDOQ6541165

Authors: Nicolas Peltier 

Publication date: 17 May 2024

Mathematics Subject Classification ID

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

Cites Work

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

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)