Skip to Main content Skip to Navigation
Conference papers

Unifying Decidable Entailments in Separation Logic with Inductive Definitions

Résumé : The entailment problem φ |= ψ in Separation Logic [12,15], between separated conjunctions of equational (x ≈y and x 6≈y), spatial (x 7→(y1,...,yκ)) and predicate (p(x1,...,xn)) atoms, interpreted by a finite set of inductive rules, is undecidable in general. Certain restrictions on the set of inductive definitions lead to decidable classes of entailment problems. Currently, there are two such decidable classes, based on two restrictions, called establishment [10,13,14] and restrictedness [8], respectively. Both classes are shown to be in 2EXPTIME by the independent proofs from [14] and [8], respectively, and a many-one reduction of established to restricted entailment problems has been given [8]. In this paper, we strictly generalize the restricted class, by distinguishing the conditions that apply only to the left- (φ) and the right- (ψ) hand side of entailments, respectively. We provide a many-one reduction of this generalized class, called safe, to the established class. Together with the reduction of established to restricted entailment problems, this new reduction closes the loop and shows that the three classes of entailment problems (respectively established, restricted and safe) form a single, unified, 2EXPTIME-complete class
Document type :
Conference papers
Complete list of metadata

https://hal.archives-ouvertes.fr/hal-03304653
Contributor : Radu Iosif Connect in order to contact the contributor
Submitted on : Wednesday, July 28, 2021 - 3:30:10 PM
Last modification on : Tuesday, October 12, 2021 - 3:19:33 AM

File

CADE_2021_final_version.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Mnacho Echenim, Radu Iosif, Nicolas Peltier. Unifying Decidable Entailments in Separation Logic with Inductive Definitions. CADE 28, 2021, Pittsburgh (virtual), United States. pp.183-199, ⟨10.1007/978-3-030-79876-5_11⟩. ⟨hal-03304653⟩

Share

Metrics

Record views

21

Files downloads

45