Talks and Poster Presentations (without Proceedings-Entry):
A. John, I. Konnov, U. Schmid, H. Veith, J. Widder:
"Counter Attack against Byzantine Generals";
Talk: Alpine Verification Meeting,
Passau, Bayern, Deutschland;
We consider automatic veriﬁcation 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 difﬁculty for model checking algorithms.
Created from the Publication Database of the Vienna University of Technology.