24 citations · 40 across the 18 of their papers we have counts for
23 papers
Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates
Mnacho Echenim, Nicolas Peltier
We establish various complexity results for the entailment problem between formulas in Separation Logic with user-defined predicates denoting recursive data structures. The conside…
Two Results on Separation Logic With Theory Reasoning
Mnacho Echenim, Nicolas Peltier
Two results are presented concerning the entailment problem in Separation Logic with inductively defined predicate symbols and theory reasoning. First, we show that the entailment…
A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning
Mnacho Echenim, Nicolas Peltier
A proof procedure, in the spirit of the sequent calculus, is proposed to check the validity of entailments between Separation Logic formulas combining inductively defined predicate…
A Superposition-Based Calculus for Quantum Diagrammatic Reasoning and Beyond
Rachid Echahed, Mnacho Echenim, Mehdi Mhalla +1
We introduce a class of rooted graphs which allows one to encode various kinds of classical or quantum circuits. We then follow a set-theoretic approach to define rewrite systems o…
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 (…
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…