Machine checked proofs of the design of a fault-tolerant circuit

DOI10.1007/BF03180571zbMath0760.68063MaRDI QIDQ1203129

William D. Young, William R. Bevier

Publication date: 4 February 1993

Published in: Formal Aspects of Computing (Search for Journal in Brave)

zbMATH Keywords

Boyer-Moore theorem proverfault-tolerant circuitfault-tolerant deviceimplementation of the oral messages algorithmmachine checked proofs

Mathematics Subject Classification ID

Uses Software

• NQTHM
• UNITY

Cites Work

• Synchronizing clocks in the presence of faults
• Impossibility of distributed consensus with one faulty process
• Reaching Agreement in the Presence of Faults
• The Byzantine Generals Problem
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Machine checked proofs of the design of a fault-tolerant circuit