{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:31:43Z","timestamp":1759638703674},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540414131"},{"type":"electronic","value":"9783540444503"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44450-5_26","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T08:26:08Z","timestamp":1187252768000},"page":"325-335","source":"Crossref","is-referenced-by-count":7,"title":["Formal Verification of the Ricart-Agrawala Algorithm"],"prefix":"10.1007","author":[{"given":"Ekaterina","family":"Sedletsky","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mordechai","family":"Ben-Ari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,11,24]]},"reference":[{"unstructured":"M. Ben-Ari. Principles of Concurrent and Distributed Programming. Prentice-Hall International, Hemel Hempstead, 1990.","key":"26_CR1"},{"unstructured":"N. Bj\u00f8rner, I.A. Browne, E. Chang, M. Col\u00f3n, A. Kapur, Z. Manna, H.B. Sipma, and T.E. Uribe. STeP: The Stanford Temporal Prover, User\u2019s Manual. Technical Report STAN-CS-TR-95-1562, Computer Science Department, Stanford University, November 1995.","key":"26_CR2"},{"unstructured":"J. Kamerer. Ricart and Agrawala\u2019s algorithm. Unpublished, \n                    http:\/\/rodin.stanford.edu\/case-studies\n                    \n                  , 9 August 1995.","key":"26_CR3"},{"issue":"3","key":"26_CR4","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/0167-6423(83)90014-X","volume":"2","author":"L. Lamport","year":"1982","unstructured":"L. Lamport An Assertional Correctness Proof of Distributed Program. Science of Computer Programming, 2, 3, December 1982, pages 175\u2013206.","journal-title":"Science of Computer Programming"},{"key":"26_CR5","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991."},{"doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Temporal verification diagrams. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software, volume 789 of Lect. Notes in Comp. Sci., pages 726\u2013765. Springer-Verlag, 1994.","key":"26_CR6","DOI":"10.1007\/3-540-57887-0_123"},{"key":"26_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995."},{"key":"26_CR8","first-page":"167","volume-title":"Specification and Validation Methods","author":"Z. Manna","year":"1995","unstructured":"Z. Manna and A. Pnueli. Verification of parameterized programs. In E. B\u00f6rger, editor, Specification and Validation Methods, pages 167\u2013230. Oxford University Press, Oxford, 1995."},{"issue":"1","key":"26_CR9","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/358527.358537","volume":"24","author":"G. Ricart","year":"1981","unstructured":"G. Ricart and A.K. Agrawala. An optimal algorithm for mutual exclusion in computer networks. Comm. ACM, 24(1):9\u201317, 1981. Corr. ibid. 1981, p.581.","journal-title":"Comm. ACM"}],"container-title":["Lecture Notes in Computer Science","FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44450-5_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,21]],"date-time":"2019-02-21T22:39:04Z","timestamp":1550788744000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44450-5_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540414131","9783540444503"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-44450-5_26","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}