@inproceedings{2a9967a7ff734a64be2d8996ba63cca5,
title = "An elementary derivation of the alternating bit protocol",
abstract = "The famous alternating bit protocol is an algorithm for transmitting a sequence of data through a so-called faulty channel, i.e. a channel that can lose or duplicate injected data. The established literature provides a wealth of treatments and plenty of a-posteriori correctness proofs of the protocol; derivations of the algorithm, however, are very rare. The prime purpose of this note is to provide such a derivation from first principles, using the theory of Owicki and Gries as the only tool for reasoning about parallel programs.",
author = "W.H.J. Feijen and {Gasteren, van}, A.J.M. and B. Schieder",
year = "1998",
doi = "10.1007/BFb0054290",
language = "English",
isbn = "3-540-64591-8",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "175--187",
editor = "J. Jeuring",
booktitle = "Mathematics of Program Construction (Proceedings 4th International Conference, MPC'98, Marstrand, Sweden, July 15-17, 1998)",
address = "Germany",
}