[Zurück]

A. John, I. Konnov, U. Schmid, H. Veith, J. Widder:
"Counter Attack against Byzantine Generals";
Vortrag: Alpine Verification Meeting, Passau, Bayern, Deutschland; 21.05.2012 - 22.05.2012.

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.