{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:15:33Z","timestamp":1725664533209},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540602187"},{"type":"electronic","value":"9783540447382"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60218-6_14","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:50:50Z","timestamp":1330260650000},"page":"190-203","source":"Crossref","is-referenced-by-count":4,"title":["Verification of a distributed summation algorithm"],"prefix":"10.1007","author":[{"given":"Frits","family":"Vaandrager","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"issue":"2","key":"14_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253\u2013284, 1991.","journal-title":"Theoretical Computer Science"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"K.M. Chandy and J. Misra. Parallel Program Design. A Foundation. Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"C.-T. Chou. Mechanical verification of distributed algorithms in higher-order logic. In T.F. Melham and J. Camilleri, editors, Proceedings 7 th International Workshop on Higher-Order Logic and its Applications, volume 859 of Lecture Notes in Computer Science, pages 158\u2013176. Springer-Verlag, 1994. A revised version will appear in The Computer Journal, 1995.","DOI":"10.1093\/comjnl\/38.2.152"},{"key":"14_CR4","unstructured":"C.-T. Chou. Practical use of the notions of events and causality in reasoning about distributed algorithms. CS Report #940035, UCLA, October 1994. Available via anonymous ftp at the URL ftp:\/\/ftp.cs.ucla.edu\/pub\/chou\/nil.ps."},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"J.F. Groote and A. Ponse. Proof theory for \u03bcCRL: A language for processes with data. In D.J. Andrews, J.F. Groote, and C.A. Middelburg, editors. Proceedings of the International Workshop on Semantics of Specification Languages, Workshops in Computer Science, pages 231\u2013250. Springer-Verlag, 1993.","DOI":"10.1007\/978-1-4471-3229-5_13"},{"key":"14_CR6","first-page":"127","volume-title":"volume 806 of Lecture Notes in Computer Science","author":"L. Helmink","year":"1994","unstructured":"L. Helmink, M.P.A. Sellink, and F.W. Vaandrager. Proof-checking a data link protocol. In H. Barendregt and T. Nipkow, editors, Proceedings International Workshop TYPES'93, Nijmegen, The Netherlands, May 1993, volume 806 of Lecture Notes in Computer Science, pages 127\u2013165. Springer-Verlag, 1994. Full version available as Report CS-R9420, CWI, Amsterdam, March 1994."},{"issue":"2","key":"14_CR7","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1145\/174662.174665","volume":"16","author":"B. Jonsson","year":"1994","unstructured":"B. Jonsson. Compositional specification and verification of distributed systems. ACM Transactions on Programming Languages and Systems, 16(2):259\u2013303, March 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"4","key":"14_CR8","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1109\/TSE.1984.5010246","volume":"10","author":"S.S. Lam","year":"1984","unstructured":"S.S. Lam and A.U. Shankar. Protocol verification via projections. IEEE Transactions on Software Engineering, 10(4):325\u2013342, July 1984.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2","key":"14_CR9","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L. Lamport","year":"1983","unstructured":"L. Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5(2):190\u2013222, 1983.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"14_CR10","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872\u2013923, March 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"14_CR11","volume-title":"Technical Report 25.085","author":"P. Lucas","year":"1968","unstructured":"P. Lucas. Two constructive realizations of the block concept and their equivalence. Technical Report 25.085, IBM Laboratory, Vienna, June 1968."},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the 6 th Annual ACM Symposium on Principles of Distributed Computing, pages 137\u2013151, August 1987. A full version is available as MIT Technical Report MIT\/LCS\/TR-387.","DOI":"10.1145\/41840.41852"},{"issue":"3","key":"14_CR13","first-page":"219","volume":"2","author":"N.A. Lynch","year":"1989","unstructured":"N.A. Lynch and M.R. Tuttle. An introduction to input\/output automata. CWI Quarterly, 2(3):219\u2013246, September 1989.","journal-title":"CWI Quarterly"},{"key":"14_CR14","volume-title":"Technical Memo MIT\/LCS\/TM-486.b (new version of TM-486)","author":"N.A. Lynch","year":"1994","unstructured":"N.A. Lynch and F.W. Vaandrager. Forward and backward simulations \u2014 part I: Untimed systems. Technical Memo MIT\/LCS\/TM-486.b (new version of TM-486), Laboratory for Computer Science, Massachusetts Institute of Technolog, Cambridge, MA, August 1994. To appear in Information and Computation."},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"14_CR16","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989."},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"T. Nipkow and K. Slind. I\/O automata in Isabelle\/HOL. In Proceedings International Workshop TYPES'94, Lecture Notes in Computer Science. Springer-Verlag, 1995. To appear.","DOI":"10.1007\/3-540-60579-7_6"},{"issue":"4","key":"14_CR18","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. Owicki","year":"1976","unstructured":"S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6(4):319\u2013340, 1976.","journal-title":"Acta Informatica"},{"issue":"2","key":"14_CR19","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1109\/TIT.1983.1056620","volume":"IT-29","author":"A. Segall","year":"1983","unstructured":"A. Segall. Distributed network protocols. IEEE Transactions on Information Theory, IT-29(2):23\u201335, January 1983.","journal-title":"IEEE Transactions on Information Theory"},{"key":"14_CR20","first-page":"305","volume-title":"volume 697 of Lecture Notes in Computer Science","author":"J. S\u00f8gaard-Andersen","year":"1993","unstructured":"J. S\u00f8gaard-Andersen, S. Garland, J. Guttag, N.A. Lynch, and A. Pogosyants. Computer-assisted simulation proofs. In C. Courcoubetis, editor, Proceedings of the 5th International Conference on Computer Aided Verification, Elounda, Greece, volume 697 of Lecture Notes in Computer Science, pages 305\u2013319. Springer-Verlag, 1993."},{"key":"14_CR21","volume-title":"Report CS-R9505","author":"F.W. Vaandrager","year":"1995","unstructured":"F.W. Vaandrager. Verification of a distributed summation algorithm. Report CS-R9505, CWI, Amsterdam, January 1995. A preliminary version appeared in K.R. Apt, A. Schrijver, N.M. Temme, editors, From Universal Morphisms to Megabytes \u2014 a Baayen Space Odyssey, pages 593\u2013608, CWI, Amsterdam, 1994."}],"container-title":["Lecture Notes in Computer Science","CONCUR '95: Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60218-6_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T04:32:10Z","timestamp":1640925130000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60218-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540602187","9783540447382"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-60218-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}