At-most-once message delivery A case study in algorithm verification

  • Butler Lampson
  • Nancy Lynch
  • Jørgen Søgaard-Andersen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)


Generic Protocol Message Delivery Forward Simulation Local Clock Refinement Mapping 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Abadi and L. Lamport. The existence of refinement mappings. In Proceedings of the 3rd Annual Symposium on Logic in Computer, pages 165–175, Edinburgh, Scotland, July 1988.Google Scholar
  2. 2.
    D. Belsnes. Single message communication. IEEE Transactions on Communications, Com-24(2), February 1976.Google Scholar
  3. 3.
    B. Liskov, L. Shrira, and J. Wroclawski. Efficient at-most-once messages based on synchronized clocks. Technical Report MIT/LCS/TR-476, Laboratory for Computer Science, Massachusetts Institute of Technology, April 1990.Google Scholar
  4. 4.
    N. Lynch and I. Saias. Distributed Algorithms. Fall 1990 Lecture Notes for 6.852. MIT/LCS/RSS 16, Massachusetts Institute of Technology, February 1992.Google Scholar
  5. 5.
    N. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. Techical Report MIT/LCS/TR-387, Laboratory for Computer Science, Massachusetts Institute Technology, Cambridge, MA, 02139, April 1987.Google Scholar
  6. 6.
    N. Lynch and M. Tuttle. An introduction to Input/Output automata. CWI-Quarterly, 2(3):219–246, September 1989.zbMATHMathSciNetGoogle Scholar
  7. 7.
    N. Lynch and F. Vaandrager. Forward and backward simulations for timing-based systems. In Proceedings of REX Workshop “Real-Time: Theory in Practice”, Mook, The Netherland, 1992. Springer-Verlag, LNCS 600.Google Scholar
  8. 8.
    F. Modugno, M. Merritt, and M. Tuttle. Time constrained automata. In CONCUR'91 Proceedings Workshop on Theories of Concurrency: Unification and Extension, Amsterdam, August 1991.Google Scholar
  9. 9.
    S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6(4):319–340, 1976.zbMATHMathSciNetCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Butler Lampson
    • 1
  • Nancy Lynch
    • 2
  • Jørgen Søgaard-Andersen
    • 2
    • 3
  1. 1.Digital Equipment Corp.Denmark
  2. 2.MITUSA
  3. 3.Department of Computer ScienceTechnical University of DenmarkDenmark

Personalised recommendations