{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:09:10Z","timestamp":1760044150627},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540584681"},{"type":"electronic","value":"9783540489849"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58468-4_159","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:15:10Z","timestamp":1330254910000},"page":"41-76","source":"Crossref","is-referenced-by-count":31,"title":["Specifying and verifying fault-tolerant systems"],"prefix":"10.1007","author":[{"given":"Leslie","family":"Lamport","sequence":"first","affiliation":[]},{"given":"Stephan","family":"Merz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"issue":"2","key":"3_CR1","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"Mart\u00edn Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253\u2013284, May 1991.","journal-title":"Theoretical Computer Science"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Mart\u00edn Abadi and Leslie Lamport. An old-fashioned recipe for real time. Research Report 91, Digital Equipment Corporation, Systems Research Center, 1992. An earlier version, without proofs, appeared in [6, pages 1\u201327].","DOI":"10.1007\/BFb0031985"},{"key":"3_CR3","unstructured":"Mart\u00edn Abadi and Leslie Lamport. Conjoining specifications. Research Report 118, Digital Equipment Corporation, Systems Research Center, 1993. To appear in ACM Transactions on Programming Languages and Systems."},{"key":"3_CR4","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1016\/S0022-0000(75)80018-3","volume":"10","author":"E. A. Ashcroft","year":"1975","unstructured":"E. A. Ashcroft. Proving assertions about parallel programs. Journal of Computer and System Sciences, 10:110\u2013135, February 1975.","journal-title":"Journal of Computer and System Sciences"},{"key":"3_CR5","volume-title":"Parallel Program Design","author":"K. M. Chandy","year":"1988","unstructured":"K. Mani Chandy and Jayadev Misra. Parallel Program Design. Addison-Wesley, Reading, Massachusetts, 1988."},{"key":"3_CR6","series-title":"Volume 600 of Lecture Notes in Computer Science","volume-title":"RealTime: Theory in Practice","year":"1992","unstructured":"J. W. de Bakker, C. Huizing, W. P. de Roever, and G. Rozenberg, editors. RealTime: Theory in Practice, volume 600 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1992. Proceedings of a REX Real-Time Workshop, held in The Netherlands in June, 1991."},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Computer-Aided Verification","author":"U. Engberg","year":"1992","unstructured":"Urban Engberg, Peter Gr\u00d8nning, and Leslie Lamport. Mechanical verification of concurrent systems with TLA. In Computer-Aided Verification, Lecture Notes in Computer Science, Berlin, Heidelberg, New York, June 1992. Springer-Verlag. Proceedings of the Fourth International Conference, CAV'92."},{"key":"3_CR8","volume-title":"Series in Computer Science","author":"C. A. R. Hoare","year":"1985","unstructured":"C. A. R. Hoare. Communicating Sequential Processes. Series in Computer Science. Prentice-Hall International, London, 1985."},{"issue":"1","key":"3_CR9","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/BF02276639","volume":"6","author":"R. Kurki-Suonio","year":"1992","unstructured":"Reino Kurki-Suonio. Operational specification with joint actions: Serializable databases. Distributed Computing, 6(1):19\u201337, 1992.","journal-title":"Distributed Computing"},{"issue":"4","key":"3_CR10","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1109\/TSE.1984.5010246","volume":"SE-10","author":"S. S. Lam","year":"1984","unstructured":"Simon S. Lam and A. Udaya Shankar. Protocol verification via projections. IEEE Transactions on Software Engineering, SE-10(4):325\u2013342, July 1984.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"3_CR11","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF02276640","volume":"6","author":"S. S. Lam","year":"1992","unstructured":"Simon S. Lam and A. Udaya Shankar. Specifying modules to satisfy interfaces: A state transition system approach. Distributed Computing, 6(1):39\u201363, 1992.","journal-title":"Distributed Computing"},{"issue":"2","key":"3_CR12","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L. Lamport","year":"1983","unstructured":"Leslie Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5(2):190\u2013222, April 1983.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"3_CR13","unstructured":"Leslie Lamport. The temporal logic of actions. Research Report 79, Digital Equipment Corporation, Systems Research Center, December 1991. To appear in ACM Transactions on Programming Languages and Systems."},{"key":"3_CR14","unstructured":"Leslie Lamport. How to write a proof. Research Report 94, Digital Equipment Corporation, Systems Research Center, February 1993. To appear in American Mathematical Monthly."},{"key":"3_CR15","series-title":"Volume 736 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/3-540-57318-6_25","volume-title":"Hybrid Systems","author":"L. Lamport","year":"1993","unstructured":"Leslie Lamport. Hybrid systems in TLA+. In Robert L. Grossman, Anil Nerode, Anders P. Ravn, and Hans Rischel, editors, Hybrid Systems, volume 736 of Lecture Notes in Computer Science, pages 77\u2013102, Berlin, Heidelberg, 1993. Springer-Verlag."},{"issue":"3","key":"3_CR16","doi-asserted-by":"crossref","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L. Lamport","year":"1982","unstructured":"Leslie Lamport, Robert Shostak, and Marshall Pease. The Byzantine generals problem. ACM Transactions on Programming Languages and Systems, 4(3):382\u2013401, July 1982.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Nancy Lynch and Mark Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the Sixth Symposium on the Principles of Distributed Computing, pages 137\u2013151. ACM, August 1987.","DOI":"10.1145\/41840.41852"},{"key":"3_CR18","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1991","unstructured":"Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, New York, 1991."},{"issue":"4","key":"3_CR19","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"SE-7","author":"J. Misra","year":"1981","unstructured":"Jayadev Misra and K. Mani Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, SE-7(4):417\u2013426, July 1981.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"3_CR20","unstructured":"Peter G. Neumann and Leslie Lamport. Highly dependable distributed systems. Technical report, SRI International, June 1983. Contract Number DAEA18-81-G-0062, SRI Project 4180."}],"container-title":["Lecture Notes in Computer Science","Formal Techniques in Real-Time and Fault-Tolerant Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58468-4_159.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:21:42Z","timestamp":1605630102000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58468-4_159"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540584681","9783540489849"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-58468-4_159","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}