{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:56:25Z","timestamp":1725663385826},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540516873"},{"type":"electronic","value":"9783540467502"}],"license":[{"start":{"date-parts":[[1989,1,1]],"date-time":"1989-01-01T00:00:00Z","timestamp":599616000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1989]]},"DOI":"10.1007\/3-540-51687-5_47","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T16:12:54Z","timestamp":1330186374000},"page":"242-253","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Designing distributed algorithms by means of formal sequentially phased reasoning"],"prefix":"10.1007","author":[{"given":"F. A.","family":"Stomp","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"W. P.","family":"de Roever","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Apt K.R., Francez N., and de Roever W.P., A proof system for communicating sequential processes, ACM TOPLAS, 2\u20133 (1980).","DOI":"10.1145\/357103.357110"},{"key":"21_CR2","unstructured":"Boruvka O., O jist\u00e9m probl\u00e9mu minim\u00e1ln\u00edm, Pr\u00e1ca Moravsk\u00e9 Pr\u00edrodovedeck\u00e9 Spolecnosti (1926) (in Czech.)."},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Back R.J.R. and Sere K., Stepwise refinement of action systems, Proc. of the international conference of mathematics and program construction (1989).","DOI":"10.1007\/3-540-51305-1_7"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Chou C.T. and Gafni E., Understanding and verifying distributed algorithms using stratified decomposition, Proc. of the ACM Symp. on Principles of Distr. Comp. (1988).","DOI":"10.1145\/62546.62556"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Chandy K.M and Lamport L., Distributed snapshots: determining global states of distributed systems, ACM Trans. on Comp. Syst. 3-1 (1985).","DOI":"10.1145\/214451.214456"},{"key":"21_CR6","unstructured":"Chandy K.M. and Misra J., Parallel program design: a foundation, Addison-Wesley Publishing Company, Inc. (1988)."},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Dijkstra E.W. and Scholten C.S., Termination detecting for diffusing computations, Letters 1\u20134 (1980).","DOI":"10.1016\/0020-0190(80)90021-6"},{"key":"21_CR8","unstructured":"Even S., Graph algorithms, Computer Science Press, Inc.(USA), (1979)."},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Elrad T. and Francez N., Decomposition of distributed programs into communication closed layers, Science of Computer programming, 2 (1982).","DOI":"10.1016\/0167-6423(83)90013-8"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Francez N., Distributed termination, ACM-TOPLAS, 2-1 (1980).","DOI":"10.1145\/357084.357087"},{"key":"21_CR11","unstructured":"Fix L. and Francez N., Semantics-driven decompositions for the verification of distributed programs, manuscript (1989)."},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Gallager R.T., Humblet P.A., and Spira P.M., A distributed algorithm for minimum-weight spanning trees, ACM TOPLAS, 5-1 (1983).","DOI":"10.1145\/357195.357200"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Gerth R.T. and Shrira L., On proving closedness of distributed layers, LNCS-241 (1986).","DOI":"10.1007\/3-540-17179-7_20"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Humblet P.A., A distributed algorithm for minimum-weight directed spanning trees, IEEE Trans. on Comm., 31-6 (1983).","DOI":"10.1109\/TCOM.1983.1095883"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Katz S. and Peled D., Interleaving set temporal logic, Proc. of the ACM Symp. on Principles of Distr. Comp. (1987).","DOI":"10.1145\/41840.41855"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Katz S. and Peled D., An efficient verification method for parallel and distributed programs, Proc. of the REX-workshop (1988).","DOI":"10.1007\/BFb0013032"},{"key":"21_CR17","unstructured":"Lamport L., Paradigms for distributed programs: computing global states. LNCS-190 (1985)."},{"key":"21_CR18","unstructured":"Manna Z. and Pnueli A., Verification of concurrent programs: A temporal proof system, Foundations of computer science IV, part 2, MC-tracts 159 (1983)."},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Merlin P.M. and Segall A., A failsafe distributed routing protocol, IEEE Trans. on Comm., 27-9 (1979).","DOI":"10.1109\/TCOM.1979.1094552"},{"key":"21_CR20","volume-title":"Compositional verification of distributed programs","author":"P.K. Pandya","year":"1988","unstructured":"Pandya P.K., Compositional verification of distributed programs, Ph.D. thesis, Tata institute of fundamental research, Bombay, India (1988)."},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Segall A., Decentralized maximum-flow algorithms, Networks 12 (1982).","DOI":"10.1002\/net.3230120302"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Segall A., Distributed network protocols, IEEE Trans. on Inf. Theory. IT29-1 (1983).","DOI":"10.1109\/TIT.1983.1056620"},{"key":"21_CR23","unstructured":"Stomp F.A. and de Roever W.P., A correctness proof of a distributed minimum-weight spanning tree algorithm (extended abstract), Proc. of the 7th ICDCS (1987)."},{"key":"21_CR24","unstructured":"Stomp F.A. and de Roever W.P., A fully worked out correctness proof of Gallager, Humblet, and Spira's minimum-weight spanning tree algorithm, Internal Report 87-4, University of Nijmegen (1987)."},{"key":"21_CR25","unstructured":"Stomp F.A. and de Roever W.P., A formalization of sequentially phased intuition in network protocols, Internal Report 88-15, University of Nijmegen (1988)."},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"Stomp F.A. and de Roever W.P., Designing distributed algorithms by means of sequentially phased reasoning (full paper), Internal Report 89-8, University of Nijmegen (1989).","DOI":"10.1007\/3-540-51687-5_47"},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"Schlichting R.D. and Schneider F.B., Using message passing for distributed programming, Proof rules and disciplines, ACM TOPLAS 6-3 (1984).","DOI":"10.1145\/579.583"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Welch J.L., Lamport L., and Lynch N.A., A lattice-structured proof of a minimum spanning tree algorithm, Proc. of the ACM Symp. on Principles of Distr. Comp. (1988).","DOI":"10.21236\/ADA198312"},{"key":"21_CR29","unstructured":"Zerbib F.B.M. and Segall A., A distributed shortest path protocol, Internal Report EE-395, Technion-Israel Institute of Technology, Haifa, Israel (1980)."}],"container-title":["Lecture Notes in Computer Science","Distributed Algorithms"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-51687-5_47","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T21:05:17Z","timestamp":1578517517000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-51687-5_47"}},"subtitle":["extended abstract"],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540516873","9783540467502"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-51687-5_47","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1989]]},"assertion":[{"value":"2 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}