Linköping University: Students Alumni Trade and Industry/Society Internal Search

Verifying Safety of Parameterized Heard-Of Algorithms

Zeinab Ganjei
Ahmed Rezine
Petru Eles Author homepage
Zebo Peng Author homepage

Networked Systems. NETYS 2020

We consider the problem of automatically checking safety properties of fault-tolerant distributed algorithms. We express the considered class of distributed algorithms in terms of the Heard-Of Model where arbitrary many processes proceed in infinite rounds in the presence of failures such as message losses or message corruptions. We propose, for the considered class, a sound but (in general) incomplete procedure that is guaranteed to terminate even in the presence of unbounded numbers of processes. In addition, we report on preliminary experiments for which either correctness is proved by our approach or a concrete trace violating the considered safety property is automatically found.

[GREP21] Zeinab Ganjei, Ahmed Rezine, Petru Eles, Zebo Peng, "Verifying Safety of Parameterized Heard-Of Algorithms", Networked Systems. NETYS 2020
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)