SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

A Formally Verified Algorithm for Interactive Consistency Under a Hybrid Fault Model (1993)
 by Dr. Patrick Lincoln & Dr. John Rushby.

From Fault-Tolerant Computing Symposium, FTCS 23.
IEEE Computer Society, Toulouse, France.
June, 1993.
Pages 402–411.


Abstract

Thambidurai and Park have proposed an algorithm for Interactive Consistency that retains resilience to the arbitrary (or Byzantine) fault mode, while tolerating more faults of simpler kinds than standard Byzantine-resilent algorithms. Unfortunately, and despite a published proof of correctness, their algorithm is flawed. We detected this while undertaking a formal verification of the algorithm.

We present a corrected algorithm that has been subjected to mechanically-checked formal verification. Because informal proofs seem unreliable in this domain, and the consequences of failure could be catastrophic, we believe formal verification should become standard for algorithms intended for safety-critical applications.

BibTEX Entry
@inproceedings{ftcs93,
    AUTHOR = {Patrick Lincoln and John Rushby},
    TITLE = {{A} Formally Verified Algorithm for Interactive Consistency Under a Hybrid Fault Model},
    BOOKTITLE = {Fault-Tolerant Computing Symposium, {FTCS} 23},
    YEAR = {1993},
    PAGES = {402--411},
    ADDRESS = {Toulouse, France},
    MONTH = {jun},
    ORGANIZATION = {{IEEE} Computer Society},
    URL = {http://www.csl.sri.com/papers/ftcs93/}
}
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy