Hierarchical correctness proofs for distributed algorithms
Nancy A. Lynch and Mark R. Tuttle
Discussion led by Andrew K. Hirsch on August 5, 2015
We introduce the input-output automaton, a simple but powerful model of computation in asynchronous distributed networks. With this model we are able to construct modular, hierarchical correctness proofs for distributed algorithms. We define this model, and give an interesting example of how it can be used to construct such proofs.