Number SRI-CSL-92-1.
Computer Science Laboratory, SRI International, Menlo Park, CA.
July, 1992.

We describe the formal specification and verification of an algorithm for Interactive Consistency based on the Oral Messages algorithm for Byzantine Agreement. We compare our treatment with that of Bevier and Young, who presented a formal specification and verification for a very similar algorithm. Unlike Bevier and Young, who observed that ``the invariant maintained in the recursive subcases of the algorithm is significantly more complicated than is suggested by the published proof'' and who found its formal verification ``a fairly difficult exercise in mechanical theorem proving,'' our treatment is very close to the previously published analysis of the algorithm, and our formal specification and verification are straightforward.

This example illustrates how delicate choices in the formulation of a problem can have significant impact on the readability of its formal specification and on the tractability of its formal verification.

@techreport{csl-92-1,
    AUTHOR = {John Rushby},
    TITLE = {Formal Verification of an Oral Messages Algorithm for Interactive Consistency},
    INSTITUTION = {Computer Science Laboratory, {SRI} International},
    YEAR = {1992},
    NUMBER = {{SRI-CSL-92-1}},
    ADDRESS = {Menlo Park, {CA}},
    MONTH = {jul},
    NOTE = {Also available as {NASA} Contractor Report 189704, October 1992},
    URL = {http://www.csl.sri.com/papers/csl-92-1/}
}

• csl-92-1.dvi
• csl-92-1.pdf
• csl-92-1.ps