%0 Report %1 Castro99acorrectness %A Castro, Miguel %A Liskov, Barbara %D 1999 %K bft ioautomata proof %T A Correctness Proof for a Practical Byzantine-Fault-Tolerant Replication Algorithm %U http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.9935 %X 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

@techreport{Castro99acorrectness, 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}, added-at = {2009-11-16T10:51:23.000+0100}, author = {Castro, Miguel and Liskov, Barbara}, biburl = {https://www.bibsonomy.org/bibtex/219d532c3e5ee77ab295b67fc050d4ae7/giuliano.losa}, description = {A Correctness Proof for a Practical Byzantine-Fault-Tolerant Replication Algorithm}, interhash = {16ca535b57130ec61a4315785b5aa560}, intrahash = {19d532c3e5ee77ab295b67fc050d4ae7}, keywords = {bft ioautomata proof}, timestamp = {2010-01-12T11:22:01.000+0100}, title = {A Correctness Proof for a Practical Byzantine-Fault-Tolerant Replication Algorithm}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.9935}, year = 1999 }