8 citations · 12 across the 8 of their papers we have counts for
12 papers · 1 filter
Proceedings 9th edition of Working Formal Methods Symposium
Andrei Arusoaie, Horaţiu Cheval, Radu Iosif
This volume contains the proceedings of the 9th Working Formal Methods Symposium, which was held at the Alexandru Ioan Cuza University, Iaşi, Romania on September 17-19, 2025.
On an Invariance Problem for Parameterized Concurrent Systems
Marius Bozga, Lucas Bueri, Radu Iosif
We consider concurrent systems consisting of replicated finite-state processes that synchronize via joint interactions in a network with user-defined topology. The system is specif…
Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems
Marius Bozga, Lucas Bueri, Radu Iosif
We consider a logic used to describe sets of configurations of distributed systems, whose network topologies can be changed at runtime, by reconfiguration programs. The logic uses…
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…
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.…