{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:32:01Z","timestamp":1750307521397,"version":"3.41.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2009,9,25]],"date-time":"2009-09-25T00:00:00Z","timestamp":1253836800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGACT News"],"published-print":{"date-parts":[[2009,9,25]]},"DOI":"10.1145\/1620491.1620507","type":"journal-article","created":{"date-parts":[[2009,10,6]],"date-time":"2009-10-06T18:18:59Z","timestamp":1254853139000},"page":"78-85","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Building reliable large-scale distributed systems"],"prefix":"10.1145","volume":"40","author":[{"given":"Lidong","family":"Zhou","sequence":"first","affiliation":[{"name":"Microsoft Research, Asia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2009,9,25]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Mark Bickford and David Guaspari. Formalizing the chain replication protocol. http:\/\/www.cs.cornell.edu\/Info\/Projects\/NuPrl\/FDLcontentAUXdocs\/ChainRepl September 2006.  Mark Bickford and David Guaspari. Formalizing the chain replication protocol. http:\/\/www.cs.cornell.edu\/Info\/Projects\/NuPrl\/FDLcontentAUXdocs\/ChainRepl September 2006."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(87)90085-7"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/4236.939450"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(87)90084-5"},{"key":"e_1_2_1_5_1","first-page":"335","volume-title":"Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI 2006","author":"Burrows Mike","year":"2006","unstructured":"Mike Burrows . The Chubby lock service for loosely-coupled distributed systems . In Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI 2006 ), pages 335 -- 350 , Berkeley, CA, USA , 2006 . USENIX Association. Mike Burrows. The Chubby lock service for loosely-coupled distributed systems. In Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI 2006), pages 335--350, Berkeley, CA, USA, 2006. USENIX Association."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2009.5270299"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson Engler . KLEE : Unassisted and automatic generation of high-coverage tests for complex systems programs . In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008) , 2008 . Cristian Cadar, Daniel Dunbar, and Dawson Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008), 2008."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/90.649465"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1281100.1281103"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the Seventh Symposium on Operating System Design and Implementation (OSDI 2006)","author":"Chang F.","year":"2006","unstructured":"F. Chang , J. Dean , S. Ghemawat , W.C. Hsieh , M. Burrows D.A. Wallach , T. Chandra , A. Fikes , and R.E. Gruber . Bigtable: A distributed storage system for structured data . In Proceedings of the Seventh Symposium on Operating System Design and Implementation (OSDI 2006) , November 2006 . F. Chang, J. Dean, S. Ghemawat, W.C. Hsieh, M. Burrows D.A. Wallach, T. Chandra, A. Fikes, and R.E. Gruber. Bigtable: A distributed storage system for structured data. In Proceedings of the Seventh Symposium on Operating System Design and Implementation (OSDI 2006), November 2006."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248119"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945450"},{"key":"e_1_2_1_13_1","volume-title":"LISA","author":"Hamilton James","year":"2007","unstructured":"James Hamilton . On designing and deploying internet-scale services . In LISA , 2007 . James Hamilton. On designing and deploying internet-scale services. In LISA, 2007."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.80192"},{"key":"e_1_2_1_15_1","volume-title":"SPIN Model Checker, The Primer and Reference Manual","author":"Holzmann Gerard J.","year":"2003","unstructured":"Gerard J. Holzmann . SPIN Model Checker, The Primer and Reference Manual . Addison-Wesley , September 2003 . Gerard J. Holzmann. SPIN Model Checker, The Primer and Reference Manual. Addison-Wesley, September 2003."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1243418.1243426"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250755"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12046-009-0002-4"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_2_1_21_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport . Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley Professional , July 2002 . Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Professional, July 2002."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1582716.1582783"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/121132.121169"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 5th Symposium on Networked Systems Design and Implementation (NSDI 2008)","author":"Liu Xuezheng","year":"2008","unstructured":"Xuezheng Liu , Zhenyu Guo , Xi Wang , Feibo Chen , Xiaochen Lian , Jian Tang , Ming Wu , M. Frans Kaashoek , and Zheng Zhang . D3S : Debugging deployed distributed systems . In Proceedings of the 5th Symposium on Networked Systems Design and Implementation (NSDI 2008) , 2008 . Xuezheng Liu, Zhenyu Guo, Xi Wang, Feibo Chen, Xiaochen Lian, Jian Tang, Ming Wu, M. Frans Kaashoek, and Zheng Zhang. D3S: Debugging deployed distributed systems. In Proceedings of the 5th Symposium on Networked Systems Design and Implementation (NSDI 2008), 2008."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217946"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480439.1480440"},{"key":"e_1_2_1_27_1","first-page":"8","volume-title":"OSDI'04: Proceedings of the 6th Conference on Symposium on Opearting Systems Design and Implementation","author":"MacCormick John","year":"2004","unstructured":"John MacCormick , Nick Murphy , Marc Najork , Chandramohan A. Thekkath , and Lidong Zhou . Boxwood : abstractions as the foundation for storage infrastructure . In OSDI'04: Proceedings of the 6th Conference on Symposium on Opearting Systems Design and Implementation , pages 8 -- 8 , Berkeley, CA, USA , 2004 . USENIX Association. John MacCormick, Nick Murphy, Marc Najork, Chandramohan A. Thekkath, and Lidong Zhou. Boxwood: abstractions as the foundation for storage infrastructure. In OSDI'04: Proceedings of the 6th Conference on Symposium on Opearting Systems Design and Implementation, pages 8--8, Berkeley, CA, USA, 2004. USENIX Association."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1326542.1326543"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1218063.1217964"},{"key":"e_1_2_1_30_1","volume-title":"OSDI","author":"Musuvathi Madanlal","year":"2008","unstructured":"Madanlal Musuvathi , Shaz Qadeer , Thomas Ball , Gerard Basler , Piramanayagam Arumuga Nainar , and Iulian Neamtiu . Finding and reproducing heisenbugs in concurrent programs . In OSDI , 2008 . Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. Finding and reproducing heisenbugs in concurrent programs. In OSDI, 2008."},{"key":"e_1_2_1_31_1","volume-title":"NSDI","author":"Reynolds Patrick","year":"2006","unstructured":"Patrick Reynolds , Charles Killian , Janet L. Wiener , Jeffrey C. Mogul , Mehul A. Shah , and Amin Vahdat . Pip : Detecting the unexpected in distributed systems . In NSDI , 2006 . Patrick Reynolds, Charles Killian, Janet L. Wiener, Jeffrey C. Mogul, Mehul A. Shah, and Amin Vahdat. Pip: Detecting the unexpected in distributed systems. In NSDI, 2006."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/98163.98167"},{"key":"e_1_2_1_34_1","volume-title":"Using Formal Description Techniques: An Introduction to Estelle, Lotos, and SDL","author":"Turner Kenneth J.","year":"1993","unstructured":"Kenneth J. Turner . Using Formal Description Techniques: An Introduction to Estelle, Lotos, and SDL . John Wiley &Sons, Inc., New York, NY, USA, 1993 . Kenneth J. Turner. Using Formal Description Techniques: An Introduction to Estelle, Lotos, and SDL. John Wiley&Sons, Inc., New York, NY, USA, 1993."},{"key":"e_1_2_1_35_1","first-page":"91","volume-title":"Proceedings of the 6th Symposium on Operating System Design and Implementation (OSDI 2004","author":"van Renesse Robbert","year":"2004","unstructured":"Robbert van Renesse and Fred B. Schneider . Chain replication for supporting high throughput and availability . In Proceedings of the 6th Symposium on Operating System Design and Implementation (OSDI 2004 ), pages 91 -- 104 , Berkeley, CA, USA , 2004 . USENIX Association. Robbert van Renesse and Fred B. Schneider. Chain replication for supporting high throughput and availability. In Proceedings of the 6th Symposium on Operating System Design and Implementation (OSDI 2004), pages 91--104, Berkeley, CA, USA, 2004. USENIX Association."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.4658"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2009","author":"Yang Junfeng","year":"2009","unstructured":"Junfeng Yang , Tisheng Chen , Ming Wu , Zhilei Xu , Xuezheng Liu , Haoxiang Lin , Mao Yang , Fan Long , Lintao Zhang , and Lidong Zhou . Modist : Transparent model checking of unmodified distributed systems . In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2009 ), Boston, MA, USA , April 2009 . USENIX. Junfeng Yang, Tisheng Chen, Ming Wu, Zhilei Xu, Xuezheng Liu, Haoxiang Lin, Mao Yang, Fan Long, Lintao Zhang, and Lidong Zhou. Modist: Transparent model checking of unmodified distributed systems. In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2009), Boston, MA, USA, April 2009. USENIX."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1281100.1281138"}],"container-title":["ACM SIGACT News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1620491.1620507","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1620491.1620507","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:18:16Z","timestamp":1750249096000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1620491.1620507"}},"subtitle":["when theory meets practice"],"short-title":[],"issued":{"date-parts":[[2009,9,25]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,9,25]]}},"alternative-id":["10.1145\/1620491.1620507"],"URL":"https:\/\/doi.org\/10.1145\/1620491.1620507","relation":{},"ISSN":["0163-5700"],"issn-type":[{"type":"print","value":"0163-5700"}],"subject":[],"published":{"date-parts":[[2009,9,25]]},"assertion":[{"value":"2009-09-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}