[Back]

A. John, I. Konnov, U. Schmid, H. Veith, J. Widder:
"Counter Attack against Byzantine Generals";
Talk: Alpine Verification Meeting, Passau, Bayern, Deutschland; 2012-05-21 - 2012-05-22.

We consider automatic verification of threshold-based fault-tolerant distributed algorithms. These algo-
rithms are parameterized in the size of the system, and the assumed maximal number of faulty processes. In order to
automatically verify such distributed algorithms, we propose a novel technique based on counter abstraction, interval
abstraction, and model checking.
We explain our method using an asynchronous broadcasting algorithm that tolerates Byzantine process faults. Al-
though the code of the original distributed algorithm is very simple, the uncertainty imposed by the asynchrony of the
processes, and the faults poses a serious difficulty for model checking algorithms.