4 citations · 8 across the 17 of their papers we have counts for
Showing 2020Show all
3 papers · 1 filter
cs.LO2020
Unifying Decidable Entailments in Separation Logic with Inductive Definitions
Mnacho Echenim, Radu Iosif, Nicolas Peltier
The entailment problem in Separation Logic \cite{IshtiaqOHearn01,Reynolds02}, between separated conjunctions of equational ($x \iseq y$ and $x \not\iseq y$), spatial (…
cs.LO2020
Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Established Systems
Mnacho Echenim, Radu Iosif, Nicolas Peltier
We define a class of Separation Logic formulae, whose entailment problem: given formulae , is every model of a model of some ? is 2EXPTIME-complete. T…
cs.LO2020
Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard
Mnacho Echenim, Radu Iosif, Nicolas Peltier
The entailment between separation logic formulae with inductive predicates, also known as symbolic heaps, has been shown to be decidable for a large class of inductive definitions.…