DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click HERE
to register or log in.
Verifying Programs That Use Causally-Ordered Message-Passing
CORNELL UNIV ITHACA NY DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
We give an operational model of causally-ordered message-passing primitives. Based on this model, we formulate a Hoare-style proof system for causally-ordered delivery. To illustrate the use of this proof system and to demonstrate the feasibility of applying invariant-based verification techniques to algorithms that depend on causally-ordered delivery, we verify an- asynchronous variant of the distributed termination detection algorithm of Dijkstra, Feijen, and van Gasteren. Verification, Message-passing, Causal delivery.
APPROVED FOR PUBLIC RELEASE