PVS Example: The Oral Messages Algorithm for Byzantine Agreement

NOTE (4/26/96): Following haven't been checked with released version
of the system owing to file system problems (I think there's one less
TCC branch in some of the proofs that with earlier versions and so the
scripts get out of synch)


Description: csl-92-1.dvi.Z and csl-92-1.ps.gz describe the
  formal specification and verification of the Interactive Consistency
  (symmetric) version of this algorithm using EHDM.   

  Appendix B sketches a Byzantine Agreement version.

  The dump file presents this version in PVS.  Readers familiar with
  PVS should be able to read the EHDM description, and vice-versa.

LaTeX-printed specifications:
  byzantine.dvi and byzantine.ps

LaTeX-printed proofs (the two main lemmas):
  C1.dvi and C1.ps
  C2.dvi and C2.ps

Dump file: byzantine.dmp
  Use M-x undump-pvs-file byzantine.dmp
