An efficient cyclic entailment procedure in a fragment of separation logic
From MaRDI portal
Publication:6091213
DOI10.1007/978-3-031-30829-1_23arXiv2210.00616OpenAlexW4366503835MaRDI QIDQ6091213
Publication date: 24 November 2023
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2210.00616
Cites Work
- Unnamed Item
- Compositional entailment checking for a fragment of separation logic
- A separation logic with data: small models and automation
- Unifying decidable entailments in separation logic with inductive definitions
- A decidable fragment in separation logic with inductive predicates and arithmetic
- Compositional satisfiability solving in separation logic
- Automated mutual explicit induction proof in separation logic
- Frame inference for inductive entailment proofs in separation logic
- Automated mutual induction proof in separation logic
- A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints
- Separation Logic Modulo Theories
- 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
- On Automated Lemma Generation for Separation Logic with Inductive Definitions
- Satisfiability Modulo Heap-Based Programs
- The Tree Width of Separation Logic with Recursive Definitions
- 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
- Automated Reasoning with Analytic Tableaux and Related Methods
- Programming Languages and Systems
- Computer Aided Verification
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- A decision procedure for string logic with quadratic equations, regular expressions and length constraints
This page was built for publication: An efficient cyclic entailment procedure in a fragment of separation logic
