BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Radu Iosif

Radu Iosif contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
Logic in Computer ScienceDistributed, Parallel, and Cluster Computing

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
6works
0followers
2topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

6 published item(s)

preprint2022arXiv

Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems

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 inductive definitions to describe networks with an unbounded number of components and interactions, written using a multiplicative conjunction, reminiscent of Bunched Implications and Separation Logic. We study the complexity of the satisfiability and entailment problems for the configuration logic under consideration. Additionally, we consider robustness properties, such as tightness (are all interactions entirely connected to components?) and degree boundedness (is every component involved in a bounded number of interactions?), the latter being an ingredient for decidability of entailments.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

On an Invariance Problem for Parameterized Concurrent Systems

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 specified using a resource logic with a multiplicative connective and inductively defined predicates, reminiscent of Separation Logic. The problem we consider is if a given formula in this logic defines an invariant, namely whether any model of the formula, following an arbitrary firing sequence of interactions, is transformed into another model of the same formula. This property, called \emph{havoc invariance}, is quintessential in proving the correctness of reconfiguration programs that change the structure of the network at runtime. We show that the havoc invariance problem is many-one reducible to the entailment problem $ϕ\models ψ$, asking if any model of $ϕ$ is also a model of $ψ$. Although, in general, havoc invariance is found to be undecidable, this reduction allows to prove that havoc invariance is in 2EXP, for a general fragment of the logic, with a 2EXP entailment problem.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

On the Expressiveness of a Logic of Separated Relations

We compare the model-theoretic expressiveness of the existential fragment of Separation Logic over unrestricted relational signatures (SLR) -- with only separating conjunction as logical connective and higher-order inductive definitions, traditionally known as the symbolic heap fragment -- with the expressiveness of (Monadic) Second Order Logic ((M)SO). While SLR and MSO are incomparable on structures of unbounded treewidth, it turns out that SLR can be embedded in SO, in general, and that MSO becomes a strict subset of SLR, when the treewidth of the models is bounded by a parameter given as input. We also discuss the problem of defining a fragment of SLR that is equivalent to MSO over models of bounded treewidth. Such a fragment would then become the most general Separation Logic with a decidable entailment problem, a key ingredient of practical verification methods for self-adapting (reconfigurable) component-based and distributed systems.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Reasoning about Reconfigurations of Distributed Systems

This paper presents a Hoare-style calculus for formal reasoning about reconfiguration programs of distributed systems. Such programs create and delete components and/or interactions (connectors) while the system components change state according to their internal behaviour. Our proof calculus uses a resource logic, in the spirit of Separation Logic, to give local specifications of reconfiguration actions. Moreover, distributed systems with an unbounded number of components are described using inductively defined predicates. The correctness of reconfiguration programs relies on havoc invariants, that are assertions about the ongoing interactions in a part of the system that is not affected by the structural change caused by the reconfiguration. We present a proof system for such invariants in an assume/rely-guarantee style. We illustrate the feasibility of our approach by proving the correctness of real-life distributed systems with reconfigurable (self-adjustable) tree architectures.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

Unifying Decidable Entailments in Separation Logic with Inductive Definitions

The entailment problem $φ\models ψ$ in Separation Logic \cite{IshtiaqOHearn01,Reynolds02}, between separated conjunctions of equational ($x \iseq y$ and $x \not\iseq y$), spatial ($x \mapsto (y_1,\ldots,y_\rank)$) and predicate ($p(x_1,\ldots,x_n)$) 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 \emph{establishment} \cite{IosifRogalewiczSimacek13,KatelaanMathejaZuleger19,PZ20} and \emph{restrictedness} \cite{EIP21a}, respectively. Both classes are shown to be in \twoexptime\ by the independent proofs from \cite{PZ20} and \cite{EIP21a}, respectively, and a many-one reduction of established to restricted entailment problems has been given \cite{EIP21a}. 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 \emph{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, \twoexptime-complete class.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard

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. Recently, a 2-EXPTIME algorithm was proposed and an EXPTIME-hard bound was established; however no precise lower bound is known. In this paper, we show that deciding entailment between predicate atoms is 2-EXPTIME-hard. The proof is based on a reduction from the membership problem for exponential-space bounded alternating Turing machines.

0 citations0 reviewsNo code linkedOpen access