A Correctness Proof for a Practical Byzantine-Fault-Tolerant Replication Algorithm

@techreport{Castro, abstract = {This paper presents a formal specification for the unoptimized version of our algorithm presented in Section 4 of [4] and proves its safety (but not its liveness.) The specification uses the I/O automaton formalism of Tuttle an Lynch [8] and the proof is based on invariant assertions and simulation relations.}, author = {Castro, M. and Liskov, B. }, citeulike-article-id = {2371105}, number = {MIT/LCS/TM-597}, posted-at = {2008-02-13 18:09:10}, priority = {3}, title = {A Correctness Proof for a Practical Byzantine-Fault-Tolerant Replication Algorithm}, url = {http://citeseer.ist.psu.edu/378859.html}, year = {1999} }

TY - RPRT ID - Castro L3 - citeulike-article-id:2371105 TI - A Correctness Proof for a Practical Byzantine-Fault-Tolerant Replication Algorithm IS - MIT/LCS/TM-597 N2 - This paper presents a formal specification for the unoptimized version of our algorithm presented in Section 4 of [4] and proves its safety (but not its liveness.) The specification uses the I/O automaton formalism of Tuttle an Lynch [8] and the proof is based on invariant assertions and simulation relations. AU - Castro, M AU - Liskov, B PY - 1999/// UR - http://citeseer.ist.psu.edu/378859.html ER -