Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics

Idan Berkovits, Marijana Lazic, Giuliano Losa +2

Verification of fault-tolerant distributed protocols is an immensely difficult task. Often, in these protocols, thresholds on set cardinalities are used both in the process code an…