{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:33:59Z","timestamp":1781238839030,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,6,3]],"date-time":"2015-06-03T00:00:00Z","timestamp":1433289600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-0963754 DGE-1256082"],"award-info":[{"award-number":["CNS-0963754 DGE-1256082"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006831","name":"U.S. Air Force","doi-asserted-by":"publisher","award":["FA8750-12-C-0174"],"award-info":[{"award-number":["FA8750-12-C-0174"]}],"id":[{"id":"10.13039\/100006831","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-12-2-0107"],"award-info":[{"award-number":["FA8750-12-2-0107"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,6,3]]},"DOI":"10.1145\/2737924.2737958","type":"proceedings-article","created":{"date-parts":[[2015,6,3]],"date-time":"2015-06-03T11:35:56Z","timestamp":1433331356000},"page":"357-368","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":183,"title":["Verdi: a framework for implementing and formally verifying distributed systems"],"prefix":"10.1145","author":[{"given":"James R.","family":"Wilcox","sequence":"first","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Doug","family":"Woos","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pavel","family":"Panchekha","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zachary","family":"Tatlock","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xi","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael D.","family":"Ernst","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Anderson","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2015,6,3]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Apr.","year":"2011","unstructured":"Amazon. Summary of the Amazon EC2 and Amazon RDS service disruption in the US East Region , Apr. 2011 . http:\/\/aws.amazon.com\/ message\/65648\/. Amazon. Summary of the Amazon EC2 and Amazon RDS service disruption in the US East Region, Apr. 2011. http:\/\/aws.amazon.com\/ message\/65648\/."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111043"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1281100.1281103"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_3_2_1_5_1","volume-title":"Implementing Mathematics with The Nuprl Proof Development System","author":"Constable R. L.","year":"1986","unstructured":"R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , and S. F. Smith . Implementing Mathematics with The Nuprl Proof Development System . Prentice Hall , 1986 . R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with The Nuprl Proof Development System. Prentice Hall, 1986."},{"key":"e_1_3_2_1_6_1","volume-title":"etcd: A highly-available key value store for shared configuration and service discovery","author":"OS.","year":"2014","unstructured":"Core OS. etcd: A highly-available key value store for shared configuration and service discovery , 2014 . CoreOS. etcd: A highly-available key value store for shared configuration and service discovery, 2014."},{"key":"e_1_3_2_1_7_1","unstructured":"https:\/\/github.com\/coreos\/etcd.  https:\/\/github.com\/coreos\/etcd."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/336431.336455"},{"key":"e_1_3_2_1_9_1","first-page":"298","volume-title":"Proceedings of the 4th Symposium on Networked Systems Design and Implementation (NSDI)","author":"Geels D.","year":"2007","unstructured":"D. Geels , G. Altekar , P. Maniatis , T. Roscoe , and I. Stoica . Friday: Global comprehension for distributed replay . In Proceedings of the 4th Symposium on Networked Systems Design and Implementation (NSDI) , pages 285\u2013 298 , Cambridge, MA , Apr. 2007 . D. Geels, G. Altekar, P. Maniatis, T. Roscoe, and I. Stoica. Friday: Global comprehension for distributed replay. In Proceedings of the 4th Symposium on Networked Systems Design and Implementation (NSDI), pages 285\u2013298, Cambridge, MA, Apr. 2007."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462178"},{"key":"e_1_3_2_1_11_1","volume-title":"Proceedings of the HotOS XIV, Santa Ana Pueblo, NM","author":"Guo Z.","year":"2013","unstructured":"Z. Guo , S. McDirmid , M. Yang , L. Zhuang , P. Zhang , Y. Luo , T. Bergan , P. Bodik , M. Musuvathi , Z. Zhang , and L. Zhou . Failure recovery: When the cure is worse than the disease . In Proceedings of the HotOS XIV, Santa Ana Pueblo, NM , May 2013 . Z. Guo, S. McDirmid, M. Yang, L. Zhuang, P. Zhang, Y. Luo, T. Bergan, P. Bodik, M. Musuvathi, Z. Zhang, and L. Zhou. Failure recovery: When the cure is worse than the disease. In Proceedings of the HotOS XIV, Santa Ana Pueblo, NM, May 2013."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_1_14_1","first-page":"133","volume-title":"Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"Hickey J. J.","year":"2009","unstructured":"J. J. Hickey , N. Lynch , and R. van Renesse . Specifications and proofs for Ensemble layers . In Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) , pages 119\u2013 133 , York, UK , Mar. 2009 . J. J. Hickey, N. Lynch, and R. van Renesse. Specifications and proofs for Ensemble layers. In Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 119\u2013133, York, UK, Mar. 2009."},{"key":"e_1_3_2_1_15_1","volume-title":"May","author":"Scalability High","year":"2011","unstructured":"High Scalability . The updated big list of articles on the Amazon outage , May 2011 . http:\/\/highscalability.com\/blog\/2011\/5\/2\/theupdated-big-list-of-articles-on-the-amazon-outage.html. High Scalability. The updated big list of articles on the Amazon outage, May 2011. http:\/\/highscalability.com\/blog\/2011\/5\/2\/theupdated-big-list-of-articles-on-the-amazon-outage.html."},{"key":"e_1_3_2_1_16_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson D.","year":"2012","unstructured":"D. Jackson . Software Abstractions: Logic, Language, and Analysis . MIT Press , Feb. 2012 . D. Jackson. Software Abstractions: Logic, Language, and Analysis. MIT Press, Feb. 2012."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250755"},{"key":"e_1_3_2_1_18_1","first-page":"256","volume-title":"Proceedings of the 4th Symposium on Networked Systems Design and Implementation (NSDI)","author":"Killian C.","year":"2007","unstructured":"C. Killian , J. W. Anderson , R. Jhala , and A. Vahdat . Life, death, and the critical transition: Finding liveness bugs in systems code . In Proceedings of the 4th Symposium on Networked Systems Design and Implementation (NSDI) , pages 243\u2013 256 , Cambridge, MA , Apr. 2007 . C. Killian, J. W. Anderson, R. Jhala, and A. Vahdat. Life, death, and the critical transition: Finding liveness bugs in systems code. In Proceedings of the 4th Symposium on Networked Systems Design and Implementation (NSDI), pages 243\u2013256, Cambridge, MA, Apr. 2007."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_20_1","volume-title":"The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport L.","year":"2002","unstructured":"L. Lamport . Specifying Systems : The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley Professional , July 2002 . L. Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Professional, July 2002."},{"key":"e_1_3_2_1_21_1","volume-title":"Apr.","author":"Lamport L.","year":"2014","unstructured":"L. Lamport . Thinking for programmers , Apr. 2014 . http:\/\/channel9.msdn.com\/Events\/Build\/2014\/3-642. L. Lamport. Thinking for programmers, Apr. 2014. http:\/\/channel9.msdn.com\/Events\/Build\/2014\/3-642."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594334"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/319151.319157"},{"key":"e_1_3_2_1_25_1","first-page":"437","volume-title":"Proceedings of the 5th Symposium on Networked Systems Design and Implementation (NSDI)","author":"Liu X.","year":"2008","unstructured":"X. Liu , Z. Guo , X. Wang , F. Chen , X. Lian , J. Tang , M. Wu , M. F. Kaashoek , and Z. Zhang . D 3 S: Debugging deployed distributed systems . In Proceedings of the 5th Symposium on Networked Systems Design and Implementation (NSDI) , pages 423\u2013 437 , San Francisco, CA , Apr. 2008 . X. Liu, Z. Guo, X. Wang, F. Chen, X. Lian, J. Tang, M. Wu, M. F. Kaashoek, and Z. Zhang. D 3 S: Debugging deployed distributed systems. In Proceedings of the 5th Symposium on Networked Systems Design and Implementation (NSDI), pages 423\u2013437, San Francisco, CA, Apr. 2008."},{"key":"e_1_3_2_1_26_1","volume-title":"Morgan Kaufmann Publishers Inc","author":"Lynch N. A.","year":"1996","unstructured":"N. A. Lynch . Distributed Algorithms . Morgan Kaufmann Publishers Inc ., San Francisco, CA, USA , 1996 . ISBN 1558603484. N. A. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1996. ISBN 1558603484."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_3_2_1_28_1","volume-title":"Sept.","author":"Newcombe C.","year":"2014","unstructured":"C. Newcombe , T. Rath , F. Zhang , B. Munteanu , M. Brooker , and M. Deardeuff . Use of formal methods at Amazon Web Services , Sept. 2014 . http:\/\/research.microsoft.com\/enus\/um\/people\/lamport\/tla\/formal-methods-amazon.pdf. C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, and M. Deardeuff. Use of formal methods at Amazon Web Services, Sept. 2014. http:\/\/research.microsoft.com\/enus\/um\/people\/lamport\/tla\/formal-methods-amazon.pdf."},{"key":"e_1_3_2_1_29_1","volume-title":"Apr.","year":"2011","unstructured":"NYTimes. Amazon\u2019s trouble raises cloud computing doubts , Apr. 2011 . http:\/\/www.nytimes.com\/2011\/04\/23\/technology\/23cloud.html. NYTimes. Amazon\u2019s trouble raises cloud computing doubts, Apr. 2011. http:\/\/www.nytimes.com\/2011\/04\/23\/technology\/23cloud.html."},{"key":"e_1_3_2_1_31_1","first-page":"319","volume-title":"Proceedings of the 2014 USENIX Annual Technical Conference","author":"Ongaro D.","year":"2014","unstructured":"D. Ongaro and J. Ousterhout . In search of an understandable consensus algorithm . In Proceedings of the 2014 USENIX Annual Technical Conference , pages 305\u2013 319 , Philadelphia, PA , June 2014 . D. Ongaro and J. Ousterhout. In search of an understandable consensus algorithm. In Proceedings of the 2014 USENIX Annual Technical Conference, pages 305\u2013319, Philadelphia, PA, June 2014."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/356698.356702"},{"key":"e_1_3_2_1_33_1","volume-title":"Proceedings of the 10th International Workshop On User Interfaces for Theorem Provers","author":"Rahli V.","year":"2012","unstructured":"V. Rahli . Interfacing with proof assistants for domain specific programming using EventML . In Proceedings of the 10th International Workshop On User Interfaces for Theorem Provers , Bremen, Germany , July 2012 . V. Rahli. Interfacing with proof assistants for domain specific programming using EventML. In Proceedings of the 10th International Workshop On User Interfaces for Theorem Provers, Bremen, Germany, July 2012."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594338"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480934"},{"key":"e_1_3_2_1_36_1","volume-title":"PI-Calculus: A Theory of Mobile Processes","author":"Sangiorgi D.","year":"2001","unstructured":"D. Sangiorgi and D. Walker . PI-Calculus: A Theory of Mobile Processes . Cambridge University Press , New York, NY, USA , 2001 . ISBN 0521781779. D. Sangiorgi and D. Walker. PI-Calculus: A Theory of Mobile Processes. Cambridge University Press, New York, NY, USA, 2001. ISBN 0521781779."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2014.45"},{"key":"e_1_3_2_1_38_1","unstructured":"Verdi. Verdi 2014. https:\/\/github.com\/uwplse\/verdi.  Verdi. Verdi 2014. https:\/\/github.com\/uwplse\/verdi."},{"key":"e_1_3_2_1_39_1","first-page":"244","volume-title":"Proceedings of the 5th Symposium on Networked Systems Design and Implementation (NSDI)","author":"Yabandeh M.","year":"2008","unstructured":"M. Yabandeh , N. Kne\u017eevi\u00b4c , D. Kosti\u00b4c , and V. Kuncak . CrystalBall: Predicting and preventing inconsistencies in deployed distributed systems . In Proceedings of the 5th Symposium on Networked Systems Design and Implementation (NSDI) , pages 229\u2013 244 , San Francisco, CA , Apr. 2008 . M. Yabandeh, N. Kne\u017eevi\u00b4c, D. Kosti\u00b4c, and V. Kuncak. CrystalBall: Predicting and preventing inconsistencies in deployed distributed systems. In Proceedings of the 5th Symposium on Networked Systems Design and Implementation (NSDI), pages 229\u2013244, San Francisco, CA, Apr. 2008."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806610"},{"key":"e_1_3_2_1_41_1","first-page":"228","volume-title":"Proceedings of the 6th Symposium on Networked Systems Design and Implementation (NSDI)","author":"Yang J.","year":"2009","unstructured":"J. Yang , T. Chen , M. Wu , Z. Xu , X. Liu , H. Lin , M. Yang , F. Long , L. Zhang , and L. Zhou . M O D IST : Transparent model checking of unmodified distributed systems . In Proceedings of the 6th Symposium on Networked Systems Design and Implementation (NSDI) , pages 213\u2013 228 , Boston, MA , Apr. 2009 . J. Yang, T. Chen, M. Wu, Z. Xu, X. Liu, H. Lin, M. Yang, F. Long, L. Zhang, and L. Zhou. M O D IST : Transparent model checking of unmodified distributed systems. In Proceedings of the 6th Symposium on Networked Systems Design and Implementation (NSDI), pages 213\u2013228, Boston, MA, Apr. 2009."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_2_1_43_1","first-page":"265","volume-title":"Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Yuan D.","year":"2014","unstructured":"D. Yuan , Y. Luo , X. Zhuang , G. R. Rodrigues , X. Zhao , Y. Zhang , P. U. Jain , and M. Stumm . Simple testing can prevent most critical failures: An analysis of production failures in distributed data-intensive systems . In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI) , pages 249\u2013 265 , Broomfield, CO , Oct. 2014 . D. Yuan, Y. Luo, X. Zhuang, G. R. Rodrigues, X. Zhao, Y. Zhang, P. U. Jain, and M. Stumm. Simple testing can prevent most critical failures: An analysis of production failures in distributed data-intensive systems. In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI), pages 249\u2013265, Broomfield, CO, Oct. 2014."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2185376.2185383"}],"event":{"name":"PLDI '15: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Portland OR USA","acronym":"PLDI '15","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2737924.2737958","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2737924.2737958","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:12:23Z","timestamp":1750212743000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2737924.2737958"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,3]]},"references-count":42,"alternative-id":["10.1145\/2737924.2737958","10.1145\/2737924"],"URL":"https:\/\/doi.org\/10.1145\/2737924.2737958","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2813885.2737958","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2015,6,3]]},"assertion":[{"value":"2015-06-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}