9 citations · 36 across the 34 of their papers we have counts for
5 papers · 1 filter
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 (…
Verifying Safety Properties of Inductively Defined Parameterized Systems
Marius Bozga, Radu Iosif
We introduce a term algebra as a new formal specification language for the coordinating architectures of distributed systems consisting of a finite yet unbounded number of componen…
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…
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.…
Structural Invariants for the Verification of Systems with Parameterized Architectures
Marius Bozga, Javier Esparza, Radu Iosif +2
We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata. Components commu…