Patrick Lincoln and John Rushby

Proceedings of the Fault-Tolerant Computing Symposium, FTCS 23, Toulouse, France, June 1993, pp. 402-411; also appears in FTCS: Highlights from 25 Years, 1995, pp. 438-447

Abstract

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.

PDF

Slides

PDF

BibTeX Entry

@string{ftcs = {Fault Tolerant Computing Symposium }}
@string{ieeecs = {IEEE Computer Society}}

@inproceedings{Lincoln&Rushby93:FTCS,
	AUTHOR = {Patrick Lincoln and John Rushby},
	TITLE = {A Formally Verified Algorithm for Interactive Consistency
		under a Hybrid Fault Model},
	PAGES = {402--411},
	CROSSREF = {FTCS23},
	NOTE = {Reprinted in~\cite[pp.\ 438--447]{FTCS-highlights}}
}

@proceedings{FTCS23,
	KEY = {FTCS-23},
	BOOKTITLE = ftcs # 23,
	TITLE = ftcs # 23,
	MONTH = jun,
	YEAR = 1993,
	ADDRESS = {Toulouse, France},
	ORGANIZATION = ieeecs,
	
}

@proceedings{FTCS-highlights,
	KEY = {FTCS-Highlights},
	TITLE = ftcs # 25 # {: Highlights from 25 Years},
	BOOKTITLE = ftcs # 25 # {: Highlights from 25 Years},
	YEAR = 1995,
	ORGANIZATION = ieeecs,
	PUBLISHER = ieeecs,
	ADDRESS = {Pasadena, CA},
	MONTH = jun
}