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 communicate by executing atomic
interactions whose participants update their states simultaneously. We
introduce an interaction logic to specify both the type of
interactions (e.g.\ rendez-vous, broadcast) and the topology of the
system (e.g.\ pipeline, ring). The logic can be easily embedded in
monadic second order logic of $\kappa\geq1$ successors (\wss{\kappa}),
and is therefore decidable.

Proving safety properties of such a parameterized system, like
deadlock freedom or mutual exclusion, requires to infer an
inductive invariant that contains all reachable states of all system instances, and
no unsafe state. We present a method to automatically synthesize
inductive invariants directly from the formula describing the interactions,
without costly fixed point iterations. We experimentally prove that
this invariant is strong enough to verify safety properties of a large number
of systems, including textbook examples (dining philosophers,
synchronization schemes), classical mutual exclusion algorithms,
cache-coherence protocols and self-stabilization algorithms, for an arbitrary
number of components.

Structural Invariants for the Verification of Systems with Parameterized Architectures

ETAPS is a confederation of several conferences, each with its own Programme Committee and Steering Committee. ETAPS is the most important and visible annual European event related to software sciences. Altogether, more than 500 researchers participate in this event every year. The confederated conferences cover various aspects of software systems, ranging from theoretical foundations to programming language developments, compiler advancements, analysis tools, formal approaches to software engineering, and security.

A gather.town room will be open during the whole conference, which can be found here:

https://gather.town/app/nSgVv0DDYoCkmdkP/ETAPS2021

Password: Luxembourg2021

This can be used to meet in the coffee breaks.

 PDF's of the papers are available on https://etaps.org/2021/programme