{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T12:17:12Z","timestamp":1778674632822,"version":"3.51.4"},"reference-count":22,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[1995,4,1]],"date-time":"1995-04-01T00:00:00Z","timestamp":796694400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1995,4,1]],"date-time":"1995-04-01T00:00:00Z","timestamp":796694400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2000,4,18]],"date-time":"2000-04-18T00:00:00Z","timestamp":956016000000},"content-version":"vor","delay-in-days":1844,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["NOOOl4-91-J-1219"],"award-info":[{"award-number":["NOOOl4-91-J-1219"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["F49620-94-I-0198"],"award-info":[{"award-number":["F49620-94-I-0198"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100004316","name":"International Business Machines Corporation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100004316","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000104","name":"National Aeronautics and Space Administration","doi-asserted-by":"publisher","award":["NAG-2-893"],"award-info":[{"award-number":["NAG-2-893"]}],"id":[{"id":"10.13039\/100000104","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCR-9003440"],"award-info":[{"award-number":["CCR-9003440"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCR-9014363"],"award-info":[{"award-number":["CCR-9014363"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[1995,4]]},"DOI":"10.1016\/0167-6423(95)00002-a","type":"journal-article","created":{"date-parts":[[2002,10,31]],"date-time":"2002-10-31T16:12:04Z","timestamp":1036080724000},"page":"105-128","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":4,"title":["Verifying programs that use causally-ordered message-passing"],"prefix":"10.1016","volume":"24","author":[{"given":"Scott D","family":"Stoller","sequence":"first","affiliation":[]},{"given":"Fred B","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"3","key":"10.1016\/0167-6423(95)00002-A_BIB1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/390017.808306","article-title":"Gypsy: A language for specification and implementation of verifiable programs","volume":"12","author":"Ambler","year":"1977","journal-title":"ACM SIGPLAN Notices"},{"issue":"3","key":"10.1016\/0167-6423(95)00002-A_BIB2","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1145\/5956.6000","article-title":"Correctness proofs of distributed termination algorithms","volume":"8","author":"Apt","year":"1986","journal-title":"ACM Trans. Programming Lang. Systems"},{"issue":"12","key":"10.1016\/0167-6423(95)00002-A_BIB3","doi-asserted-by":"crossref","DOI":"10.1145\/163298.163303","article-title":"The process group approach to reliable distributed computing","volume":"36","author":"Birman","year":"1993","journal-title":"Comm. ACM"},{"issue":"3","key":"10.1016\/0167-6423(95)00002-A_BIB4","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1145\/128738.128742","article-title":"Lightweight causal and atomic group multicast","volume":"9","author":"Birman","year":"1991","journal-title":"ACM Trans. Comput. Systems"},{"key":"10.1016\/0167-6423(95)00002-A_BIB5","series-title":"Technical Report LITP 92-77","article-title":"Synchronous and asynchronous communication in distributed computations","author":"Charron-Bost","year":"1992"},{"issue":"4","key":"10.1016\/0167-6423(95)00002-A_BIB6","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1109\/32.223804","article-title":"Proof rules for flush channels","volume":"19","author":"Camp","year":"1993","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0167-6423(95)00002-A_BIB7","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0020-0190(83)90092-3","article-title":"Derivation of a termination detection algorithm for distributed computations","volume":"16","author":"Dijkstra","year":"1983","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/0167-6423(95)00002-A_BIB8","series-title":"Proc. 11th Australian Computer Science Conference","first-page":"56","article-title":"Timestamps in message-passing systems that preserve the partial ordering","author":"Fidge","year":"1988"},{"key":"10.1016\/0167-6423(95)00002-A_BIB9","series-title":"Conf. Record of the Sixth Ann. ACM Symp. on Principles of Programming Languages","first-page":"42","article-title":"Principles of proving concurrent programs in Gypsy","author":"Good","year":"1979"},{"key":"10.1016\/0167-6423(95)00002-A_BIB10","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1109\/TSE.1976.233828","article-title":"An illustration of current ideas on the derivation of correctness proofs and correct programs","volume":"2","author":"Gries","year":"1976","journal-title":"IEEE Trans. on Software Eng."},{"key":"10.1016\/0167-6423(95)00002-A_BIB11","series-title":"Specification and Verification of Concurrent Systems: Proc. of a 1988 BCS-FACS Workshop","article-title":"From synchronous to asynchronous communication","volume":"Vol. 1","author":"Gribomont","year":"1990"},{"issue":"10","key":"10.1016\/0167-6423(95)00002-A_BIB12","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Comm. ACM"},{"issue":"7","key":"10.1016\/0167-6423(95)00002-A_BIB13","doi-asserted-by":"crossref","first-page":"558","DOI":"10.1145\/359545.359563","article-title":"Time, clocks, and the ordering of events in a distributed system","volume":"21","author":"Lamport","year":"1978","journal-title":"Comm. ACM"},{"key":"10.1016\/0167-6423(95)00002-A_BIB14","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/BF00289062","article-title":"The \u2018Hoare logic\u2019 of concurrent programs","volume":"14","author":"Lamport","year":"1980","journal-title":"Acta Inform."},{"key":"10.1016\/0167-6423(95)00002-A_BIB15","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/BF00289266","article-title":"A proof technique for communicating sequential processes","volume":"15","author":"Levin","year":"1981","journal-title":"Acta Inform."},{"key":"10.1016\/0167-6423(95)00002-A_BIB16","series-title":"Proc. Internat. Workshop on Parallel and Distributed Algorithms","first-page":"120","article-title":"Virtual time and global states of distributed systems","author":"Mattern","year":"1989"},{"key":"10.1016\/0167-6423(95)00002-A_BIB17","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","article-title":"An axiomatic proof technique for parallel programs I","volume":"6","author":"Owicki","year":"1976","journal-title":"Acta Inform."},{"key":"10.1016\/0167-6423(95)00002-A_BIB18","series-title":"Synchronization and Control of Distributed Systems and Programs","author":"Raynal","year":"1990"},{"issue":"3","key":"10.1016\/0167-6423(95)00002-A_BIB19","doi-asserted-by":"crossref","first-page":"402","DOI":"10.1145\/579.583","article-title":"Using message passing for distributed programming: proof rules and disciplines","volume":"6","author":"Schlichting","year":"1984","journal-title":"ACM Trans. Programming Lang. Systems"},{"key":"10.1016\/0167-6423(95)00002-A_BIB20","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1016\/0020-0190(90)90027-U","article-title":"Comments on \u201cOn the proof of a distributed algorithm\u201d: Always-true is not invariant","volume":"35","author":"van Gasteren","year":"1990","journal-title":"Inform. Process. Lett."},{"issue":"2","key":"10.1016\/0167-6423(95)00002-A_BIB21","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1145\/155848.155857","article-title":"Causal controversy at le Mont St.-Michel","volume":"27","author":"van Renesse","year":"1993","journal-title":"Operating Systems Review"},{"key":"10.1016\/0167-6423(95)00002-A_BIB22","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/0020-0190(87)90123-2","article-title":"On the proof of a distributed algorithm","volume":"25","author":"Verjus","year":"1987","journal-title":"Inform. Process. Lett."}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:016764239500002A?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:016764239500002A?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T11:38:06Z","timestamp":1778672286000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/016764239500002A"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,4]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1995,4]]}},"alternative-id":["016764239500002A"],"URL":"https:\/\/doi.org\/10.1016\/0167-6423(95)00002-a","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[1995,4]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Verifying programs that use causally-ordered message-passing","name":"articletitle","label":"Article Title"},{"value":"Science of Computer Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/0167-6423(95)00002-A","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 1995 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}