{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:10:35Z","timestamp":1725466235514},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646754"},{"type":"electronic","value":"9783540691105"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054269","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T03:28:51Z","timestamp":1149650931000},"page":"317-332","source":"Crossref","is-referenced-by-count":11,"title":["A proof environment for the development of group communication systems"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Kreitz","sequence":"first","affiliation":[]},{"given":"Mark","family":"Hayden","sequence":"additional","affiliation":[]},{"given":"Jason","family":"Hickey","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"30_CR1","volume-title":"Technical report","author":"M. Archer","year":"1997","unstructured":"M. Archer & C. Heitmeyer. Mechanical verification of timed automata: A case study. Technical report, Naval Research Laboratory, Washington, DC, 1997."},{"key":"30_CR2","doi-asserted-by":"crossref","unstructured":"W. Bibel, D. Korn, C. Kreitz, F. Kurucz, J. Otten, S. Schmitt, G. Stolpmann. A multi-level approach to program synthesis. In Seventh International Workshop on Logic Program Synthesis and Transformation, LNAI, Springer Verlag, 1998.","DOI":"10.1007\/3-540-49674-2_1"},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"K. Birman. Building Secure and Reliable Network Applications. Manning Publishing Company and Prentice Hall, 1997.","DOI":"10.1007\/3-540-63343-X_35"},{"key":"30_CR4","unstructured":"K. Birman & R. van Renesse. Reliable Distributed Computing with the Isis Toolkit. IEEE Computer Society Press, 1994."},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"T. Chandra, V. Hadzilacos, S. Toueg, B. Charron-Bost. On the impossibility of group membership. 15th ACM Symposium on Principles of Distributed Computing, pp. 322\u2013330, 1996.","DOI":"10.1145\/248052.248120"},{"key":"30_CR6","unstructured":"R. Constable, et. al., Implementing Mathematics with the NuPRL proof development system. Prentice Hall, 1986."},{"key":"30_CR7","unstructured":"D. de Rauglaudre. Camlp4 version 1.06. Institut National de Recherche en Informatique et en Automatique, 1997."},{"key":"30_CR8","doi-asserted-by":"crossref","unstructured":"A. Fekete, N. Lynch, A. Shvartsman. Specifying and using a partitionable group communication service. In 16th ACM Symposium on Principles of Distributed Computing, 1997.","DOI":"10.1145\/259380.259422"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"M. Gordon, R. Milner, C. Wadsworth. Edinburgh LCF: A mechanized Logic of Computation. LNCS 78, Springer Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"30_CR10","unstructured":"O. Hafizogullari & C. Kreitz. Dead Code Elimination Through Type Inference. Technical Report TR 98-1698, Cornell University, 1998."},{"key":"30_CR11","unstructured":"M. Hayden. Ensemble Reference Manual. Cornell University, 1996."},{"key":"30_CR12","unstructured":"The Ensemble distributed communication system. System distribution and related information. http:\/\/www.cs.cornell.edu\/Info\/Projects\/Ensemble"},{"issue":"1","key":"30_CR13","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1093\/jigpal\/4.1.75","volume":"4","author":"C. Kreitz","year":"1996","unstructured":"C. Kreitz. Formal mathematics for verifiably correct program synthesis. Journal of the IGPL, 4(1):75\u201394, 1996.","journal-title":"Journal of the IGPL"},{"key":"30_CR14","unstructured":"C. Kreitz. Formal reasoning about communication systems I: Embedding ML into type theory. Technical Report TR97-1637, Cornell University, 1997."},{"key":"30_CR15","doi-asserted-by":"crossref","unstructured":"C. Kreitz, J. Otten, S. Schmitt. Guiding Program Development Systems by a Connection Based Proof Strategy. In 5th International Workshop on Logic Program Synthesis and Transformation, LNCS 1048, pp. 137\u2013151. Springer Verlag, 1996.","DOI":"10.1007\/3-540-60939-3_10"},{"key":"30_CR16","unstructured":"X. Leroy. The Objective Caml system release 1.06. Institut National de Recherche en Informatique et en Automatique, 1997."},{"key":"30_CR17","unstructured":"N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, 1996."},{"key":"30_CR18","doi-asserted-by":"crossref","unstructured":"P. Lincoln & J. Rushby. A formally verified algorithm for interactive consistency under a hybrid fault model. In 23rd Fault-Tolerant Computing Symposium, pp. 402\u2013411, 1993.","DOI":"10.1109\/FTCS.1993.627343"},{"key":"30_CR19","unstructured":"J. Rushby. Formal methods for dependable real-time systems. In International Symposium on Real-Time Embedded Processing for Space Applications, pp. 355\u2013366, 1992."},{"key":"30_CR20","unstructured":"J. Rushby. Systematic formal verification for fault-tolerant time-triggered algorithms. In Dependable Computing for Critical Applications: 6, pp. 191\u2013210. IEEE Computer Society, 1997."},{"issue":"4","key":"30_CR21","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/227210.227229","volume":"39","author":"R. Renesse van","year":"1996","unstructured":"R. van Renesse, K. Birman, & S. Maffeis. Horus: A flexible group communication system. Communications of the ACM, 39(4):76\u201383, 1996.","journal-title":"Communications of the ACM"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054269","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,10]],"date-time":"2019-02-10T18:21:00Z","timestamp":1549822860000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0054269"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/bfb0054269","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}