The design is carried out formally and rigorously. This paper
includes formal specifications of both safety and liveness properties.
The algorithm is formally modeled and assertionally verified.
20th International Conference on Distributed Computing Systems (ICDCS), April 2000: (12 pages) | ps, pdf, ps.gz |
A Virtually Synchronous Group Multicast Algorithm for WANs: Formal Approach. SIAM Journal on Computing. Volume 32. Number 1. pp. 78-130, 2002.: | ps, pdf, ps.gz |
Journal version submitted to SIAM JComp September 2000): (more discussion, explanations, and proofs, 55 pages) | ps, pdf, ps.gz |
Technical Report (MIT-LCS-TR-794, November 1999): | ps, pdf, ps.gz |