{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:49:53Z","timestamp":1762458593976},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540657033"},{"type":"electronic","value":"9783540490593"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-49059-0_9","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T21:56:57Z","timestamp":1194991017000},"page":"119-134","source":"Crossref","is-referenced-by-count":9,"title":["Specifications and Proofs for Ensemble Layers"],"prefix":"10.1007","author":[{"given":"Jason","family":"Hickey","sequence":"first","affiliation":[]},{"given":"Nancy","family":"Lynch","sequence":"additional","affiliation":[]},{"given":"Robbert","family":"van Renesse","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,3,12]]},"reference":[{"unstructured":"Emmanuelle Anceaume, Bernadette Charron-Bost, Pascale Minet, and Sam Toueg. On the formal specification of group membership services. Technical Report TR 95-1534, Cornell University Computer Science Department, August 1995.","key":"9_CR1"},{"unstructured":"Ozalp Babaoglu, Renzo Davoli, L. Giachini, and G. Baker. System support for partition-aware network applications. In Proceedings of the 18th IEEE International Conference on Distributed Computing Systems, May 1998.","key":"9_CR2"},{"doi-asserted-by":"crossref","unstructured":"Kenneth P. Birman. Building Secure and Reliable Network Applications. Manning Publishing Company and Prentice Hall, January 1997.","key":"9_CR3","DOI":"10.1007\/3-540-63343-X_35"},{"doi-asserted-by":"crossref","unstructured":"Kenneth P. Birman and Thomas A. Joseph. Exploiting virtual synchrony in distributed systems. In Proc 11th Symposium on Operating Systems Principles (SOSP), pages 123\u2013138, November 1987.","key":"9_CR4","DOI":"10.21236\/ADA177091"},{"unstructured":"R. L. Constable et.al. Implementing Mathematics in the NuPRL Proof Development System. Prentice-Hall, 1986.","key":"9_CR5"},{"issue":"8","key":"9_CR6","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1109\/2.223535","volume":"26","author":"A. Fekete","year":"1993","unstructured":"Alan Fekete. Formal models of communications services: A case study. IEEE Computer, 26(8):37\u201347, August 1993.","journal-title":"IEEE Computer"},{"doi-asserted-by":"crossref","unstructured":"Alan Fekete, Nancy Lynch, and Alex Shvartsman. Specifying and using partitionable group communication service. In Proc.16thAnnual ACM Symposium on Principles of Dist. Comp., pages 52\u201362, 1997.","key":"9_CR7","DOI":"10.1145\/259380.259422"},{"unstructured":"Mark G. Hayden. The Ensemble System. PhD thesis, Dept. of Computer Science, Cornell University, January 1997.","key":"9_CR8"},{"doi-asserted-by":"crossref","unstructured":"Jason Hickey, Nancy Lynch, and Robbert van Renesse. Specifications and proofs for Ensemble layers. Technical Report forthcoming, MIT and Cornell University, 1998. available at http:\/\/ www.cs.cornell.edu\/jyh\/papers\/HLR98.ps .","key":"9_CR9","DOI":"10.1007\/3-540-49059-0_9"},{"issue":"2","key":"9_CR10","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1145\/174662.174665","volume":"16","author":"B. Jonsson","year":"1994","unstructured":"Bengt 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"},{"unstructured":"David A. Karr. Protocol Composition on Horus. PhD thesis, Dept. of Computer Science, Cornell University, December 1996.","key":"9_CR11"},{"key":"9_CR12","series-title":"Technical Report","volume-title":"Introduction to TLA","author":"L. Lamport","year":"1994","unstructured":"Leslie Lamport. Introduction to TLA. Technical Report 1994-001, DIGITAL SRC, Palo Alto, CA, 1994."},{"issue":"3","key":"9_CR13","first-page":"219","volume":"2","author":"N. Lynch","year":"1989","unstructured":"Nancy Lynch and Mark Tuttle. An introduction to Input\/Output automata. Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands, 2(3):219\u2013246, September 1989. Also Tech. Memo MIT\/LCS\/TM-373.","journal-title":"Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands"},{"unstructured":"Nancy A. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996.","key":"9_CR14"},{"doi-asserted-by":"crossref","unstructured":"Gil Neiger. A new look at membership services. In Proc.15thAnnual ACM Symposium on Principles of Dist. Comp., pages 331\u2013340, May 1996.","key":"9_CR15","DOI":"10.1145\/248052.248121"},{"issue":"9","key":"9_CR16","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1002\/(SICI)1097-024X(19980725)28:9<963::AID-SPE179>3.0.CO;2-9","volume":"29","author":"R. Renesse Van","year":"1998","unstructured":"Robbert Van Renesse, Ken Birman, Mark Hayden, Alexey Vaysburd, and David Karr. Building adaptive systems using Ensemble. Software-Practice and Experience, 29(9):963\u2013979, July 1998.","journal-title":"Software-Practice and Experience"},{"doi-asserted-by":"crossref","unstructured":"Robbert Van Renesse, Kenneth P. Birman, Roy Friedman, Mark Hayden, and David A. Karr. A Framework for Protocol Composition in Horus. In Proc. 14th Annual ACM Symposium on Principles of Dist. Comp., pages 80\u201389, Ottawa, Ontario, August 1995. ACM SIGOPS-SIGACT.","key":"9_CR17","DOI":"10.1145\/224964.224974"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49059-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,27]],"date-time":"2021-08-27T13:54:14Z","timestamp":1630072454000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49059-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540657033","9783540490593"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-49059-0_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}