DELZANNO , Giorgio

We study parameterized verification problems for concurrent systems with data enriched with a permission model for invoking remote services. Processes are modelled via register automata. Communication is achieved by rendez-vous with value passing. Permissions are represented as graphs with an additional conflict relation to specify incompatible...

We report on recent research lines related to parameterized verification and model checking applied to formal models of distributed algorithms. Both approaches are based on graph rewriting and graph transformation systems. Case-studies include distributed mutual exclusion protocols like Ricart-Agrawala, routing protocols like link reversal, and...

We present a framework for the specification of distributed protocols based on a logic-based presentation of bipartite graphs. For the considered language, we define assertions that can be applied to arbitrary configurations. We apply the language to model the distributed version of the Dining Philosopher Protocol. The protocol is defined for...

We introduce a new class of graph transformation systems in which rewrite rules can be guarded by universally quantified conditions on the neighbourhood of nodes. These conditions are defined via special graph patterns which may be transformed by the rule as well. For the new class for graph rewrite rules, we provide a symbolic procedure...

Proceedings del workshop RP 2011

We introduce a logic-based formalism to specify updates on arbitrary graphs. For the resulting language called GLog, we introduce an assertional language for reasoning about infinite sets of graph configurations in which we use reachability predicates to specify paths of arbitrary length. For the considered assertional language and a restricted...

We present a logic-based framework for the specification and validation of distributed protocols. Our specification language is a logic-based presentation of update rules for arbitrary graphs. Update rules are specified via conditional rewriting rules defined over a relational language. We focus our attention on unary and binary relations as a...

We present a logic-based framework for the specification and validation of distributed protocols. Our specification language is a logic-based presentation of update rules for arbitrary graphs. Update rules are specified via conditional rewriting rules defined over a relational language. We focus our attention on unary and binary relations as a...

We give a unified view of different parameterized models of concurrent and distributed systems with broadcast communication based on transition systems. Based on the resulting formal models, we discuss related verification methods and tools based on abstractions and symbolic state exploration.