Verifying programs that use causally-ordered message-passing

Scott D. Stoller; Fred B. Schneider

doi:10.1016/0167-6423(95)00002-A

Verifying programs that use causally-ordered message-passing

Scott D. Stoller
, Fred B. Schneider

Computer Science

Cornell University

Research output: Contribution to journal › Article › peer-review

4 Scopus citations

Abstract

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.

Original language	English
Pages (from-to)	105-128
Number of pages	24
Journal	Science of Computer Programming
Volume	24
Issue number	2
DOIs	https://doi.org/10.1016/0167-6423(95)00002-A
State	Published - Apr 1995

Access to Document

10.1016/0167-6423(95)00002-A

Cite this

@article{456fdee855c0496299e5c265c98fa942,

title = "Verifying programs that use causally-ordered message-passing",

abstract = "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.",

author = "Stoller, \{Scott D.\} and Schneider, \{Fred B.\}",

year = "1995",

month = apr,

doi = "10.1016/0167-6423(95)00002-A",

language = "English",

volume = "24",

pages = "105--128",

journal = "Science of Computer Programming",

issn = "0167-6423",

number = "2",

}

TY - JOUR

T1 - Verifying programs that use causally-ordered message-passing

AU - Stoller, Scott D.

AU - Schneider, Fred B.

PY - 1995/4

Y1 - 1995/4

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/0029289268

U2 - 10.1016/0167-6423(95)00002-A

DO - 10.1016/0167-6423(95)00002-A

M3 - Article

AN - SCOPUS:0029289268

SN - 0167-6423

VL - 24

SP - 105

EP - 128

JO - Science of Computer Programming

JF - Science of Computer Programming

IS - 2

ER -

Verifying programs that use causally-ordered message-passing

Abstract

Access to Document

Other files and links

Fingerprint

Cite this