William R. Bevier
Research Subjects
Research Interests
William R. Bevier has a total of 1 co-authors. Here are the top co-authors by number of shared publications:
- William D. Young
Computational Logic, Inc., 1717 West Sixth Street, Suite 290, 78703-4776, Austin, Texas, USA
1 shared publication
Latest Publications
- Open Access
- 1 November 1992
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 4 (Suppl 1) , 755-775
Machine checked proofs of the design of a fault-tolerant circuit
We describe a formally verified implementation of the “Oral Messages” algorithm of Pease, Shostak and Lamport J. ACM (1980) 27 , 228–234; ACM TOPLAS (1982) 4 , 382–401. An abstract implementation of the algorithm is proved to achieve interactive consistency in the presence of faults. This abstract characterisation is then mapped down to a hardware level implementation which inherits the fault-tolerant characteristics of the abstract version. All steps in the proof were checked with the Boyer-Moore theorem prover. A significant result of this work is the demonstration of a fault-tolerant device that is formally specified and the development of an implementation proved correct with respect to this specification. A significant simplifying assumption is that the redundant processors behave synchronously. We also describe a mechanically checked proof that the Oral Messages algorithm is “optimal” in the sense that no algorithm which achieves agreement via similar message passing can tolerate a larger proportion of faulty processors.
- 1 November 1992
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 4 (Suppl 1) , 755-775
Open AccessMachine checked proofs of the design of a fault-tolerant circuit
We describe a formally verified implementation of the “Oral Messages” algorithm of Pease, Shostak and Lamport J. ACM (1980) 27 , 228–234; ACM TOPLAS (1982) 4 , 382–401. An abstract implementation of the algorithm is proved to achieve interactive consistency in the presence of faults. This abstract characterisation is then mapped down to a hardware level implementation which inherits the fault-tolerant characteristics of the abstract version. All steps in the proof were checked with the Boyer-Moore theorem prover. A significant result of this work is the demonstration of a fault-tolerant device that is formally specified and the development of an implementation proved correct with respect to this specification. A significant simplifying assumption is that the redundant processors behave synchronously. We also describe a mechanically checked proof that the Oral Messages algorithm is “optimal” in the sense that no algorithm which achieves agreement via similar message passing can tolerate a larger proportion of faulty processors.