A Case Study in the Mechanical Verification of Fault Tolerance

To date, there is little evidence that modular reasoning about fault-tolerant systems can simplify the verification process in practice. We study this question using a prominent example from the fault tolerance literature: the problem of reliable broadcast in point-to-point networks opposed to crash failures of processes. The experiences from this case study show how modular specification techniques and rigorous proof reuse can indeed help in such undertakings.

• Type: Conference
• Year: 2000
• Where: FLAIRS
• Authors: Heiko Mantel, Felix C. Gärtner
• Keywords: Artificial Intelligence, FLAIRS 2000, Modular Reasoning, Modular Specification Techniques, Rigorous Proof Reuse