Unifying decidable entailments in separation logic with inductive definitions
type: Item
instance of: scholarly article
title: Unifying decidable entailments in separation logic with inductive definitions
DOI: 10.1007/978-3-030-79876-5_11
author: Mnacho Echenim
author: Radu Iosif
author: Nicolas Peltier
publication date: 2021-12-01T00:00:00Z
full work available at URL: https://arxiv.org/abs/2012.14361
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7437079
MaRDI profile type: Publication
OpenAlex ID: W3183368753
cites work: Foundations for Decision Problems in Separation Logic with General Inductive Predicates
cites work: The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates
cites work: Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules
cites work: The Tree Width of Separation Logic with Recursive Definitions
cites work: Deciding Entailments in Inductive Separation Logic with Tree Automata
cites work: BI as an assertion language for mutable data structures
cites work: Automated mutual induction proof in separation logic
Recommended article: Effective entailment checking for separation logic with inductive definitions
Recommended article: Foundations for Decision Problems in Separation Logic with General Inductive Predicates
Recommended article: A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
Recommended article: A decision procedure for satisfiability in separation logic with inductive predicates
Recommended article: Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
Recommended article: An undecidability result for separation logic with theory reasoning
Recommended article: Q5111651
Recommended article: Deciding Entailments in Inductive Separation Logic with Tree Automata
Recommended article: Separation Logic with Monadic Inductive Definitions and Implicit Existentials
Recommended article: A proof procedure for separation logic with inductive definitions and data
description: scientific article; zbMATH DE number 7437079