A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
From MaRDI portal
Publication:5875940
DOI10.1145/3534927OpenAlexW4296613475MaRDI QIDQ5875940
Christoph Matheja, Florian Zuleger, Jens Pagel
Publication date: 7 February 2023
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2002.01202
Related Items
A proof procedure for separation logic with inductive definitions and data, An efficient cyclic entailment procedure in a fragment of separation logic, Foundations for entailment checking in quantitative separation logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- HIP
- Smallfoot
- GRASShopper
- On the almighty wand
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Constructive versions of Tarski's fixed point theorems
- Unifying decidable entailments in separation logic with inductive definitions
- A decidable fragment in separation logic with inductive predicates and arithmetic
- Automated mutual explicit induction proof in separation logic
- Automated mutual induction proof in separation logic
- Viper: A Verification Infrastructure for Permission-Based Reasoning
- Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
- Tractable Reasoning in a Fragment of Separation Logic
- Deciding Entailments in Inductive Separation Logic with Tree Automata
- Formalised Inductive Reasoning in the Logic of Bunched Implications
- Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic
- A decision procedure for satisfiability in separation logic with inductive predicates
- The Tree Width of Separation Logic with Recursive Definitions
- The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates
- BI as an assertion language for mutable data structures
- Automated Cyclic Entailment Proofs in Separation Logic
- Compositional Shape Analysis by Means of Bi-Abduction
- Foundations for Decision Problems in Separation Logic with General Inductive Predicates
- Shape Analysis for Composite Data Structures
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Programming Languages and Systems
- Program Logics for Certified Compilers
