{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:10:09Z","timestamp":1750223409472,"version":"3.41.0"},"reference-count":16,"publisher":"Association for Computing Machinery (ACM)","issue":"9","license":[{"start":{"date-parts":[[2015,11,1]],"date-time":"2015-11-01T00:00:00Z","timestamp":1446336000000},"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":["Queue"],"published-print":{"date-parts":[[2015,11]]},"abstract":"<jats:p>Leslie Lamport, known for his seminal work in distributed systems, famously said, \"A distributed system is one in which the failure of a computer you didn\u2019t even know existed can render your own computer unusable.\" Given this bleak outlook and the large set of possible failures, how do you even begin to verify and validate that the distributed systems you build are doing the right thing?<\/jats:p>","DOI":"10.1145\/2857274.2889274","type":"journal-article","created":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T15:01:36Z","timestamp":1558018896000},"page":"150-160","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["The Verification of a Distributed System"],"prefix":"10.1145","volume":"13","author":[{"given":"Caitie","family":"McCaffrey","sequence":"first","affiliation":[{"name":"Twitter"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2723372.2723711"},{"key":"e_1_2_1_2_1","unstructured":"Aniszczyk C. 2012. Distributed systems tracing with Zipkin; https:\/\/blog.twitter.com\/2012\/distributed-systems-tracing-with-zipkin.  Aniszczyk C. 2012. Distributed systems tracing with Zipkin; https:\/\/blog.twitter.com\/2012\/distributed-systems-tracing-with-zipkin."},{"key":"e_1_2_1_3_1","unstructured":"Aphyr. Jepsen; https:\/\/aphyr.com\/tags\/Jepsen.  Aphyr. Jepsen; https:\/\/aphyr.com\/tags\/Jepsen."},{"key":"e_1_2_1_4_1","unstructured":"Hedlund M. 2014. Game day exercises at Stripe: learning from \"kill -9\"; https:\/\/stripe.com\/blog\/game-day-exercises-at-stripe.  Hedlund M. 2014. Game day exercises at Stripe: learning from \"kill -9\"; https:\/\/stripe.com\/blog\/game-day-exercises-at-stripe."},{"key":"e_1_2_1_5_1","unstructured":"Izrailevsky Y. Tseitlin A. 2011. The Netflix Simian Army; http:\/\/techblog.netflix.com\/2011\/07\/netflix-simian-army.html.  Izrailevsky Y. Tseitlin A. 2011. The Netflix Simian Army; http:\/\/techblog.netflix.com\/2011\/07\/netflix-simian-army.html."},{"key":"e_1_2_1_6_1","unstructured":"Killian C. Anderson J. W. Jhala R. Vahdat A. 2006. Life death and the critical transition: finding liveness bugs in system code; http:\/\/www.macesystems.org\/papers\/MaceMC_TR.pdf.  Killian C. Anderson J. W. Jhala R. Vahdat A. 2006. Life death and the critical transition: finding liveness bugs in system code; http:\/\/www.macesystems.org\/papers\/MaceMC_TR.pdf."},{"key":"e_1_2_1_7_1","unstructured":"Lamport L. Yu Y. 2011. TLC the TLA+ model checker; http:\/\/research.microsoft.com\/en-us\/um\/people\/lamport\/tla\/tlc.html.  Lamport L. Yu Y. 2011. TLC the TLA+ model checker; http:\/\/research.microsoft.com\/en-us\/um\/people\/lamport\/tla\/tlc.html."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_2_1_9_1","unstructured":"QuickCheck; https:\/\/hackage.haskell.org\/package\/QuickCheck.  QuickCheck; https:\/\/hackage.haskell.org\/package\/QuickCheck."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2742694.2745385"},{"key":"e_1_2_1_11_1","unstructured":"Spin; http:\/\/spinroot.com\/spin\/whatispin.html.  Spin; http:\/\/spinroot.com\/spin\/whatispin.html."},{"key":"e_1_2_1_12_1","unstructured":"Sigelman B. H. Barroso L. S. Burrows M. Stephenson P. Plakal M. Beaver D. Jaspan S. Shanbhag C. 2010. Dapper a large-scale distributed systems tracing infrastructure; http:\/\/research.google.com\/pubs\/pub36356.html.  Sigelman B. H. Barroso L. S. Burrows M. Stephenson P. Plakal M. Beaver D. Jaspan S. Shanbhag C. 2010. Dapper a large-scale distributed systems tracing infrastructure; http:\/\/research.google.com\/pubs\/pub36356.html."},{"key":"e_1_2_1_13_1","unstructured":"Thompson A. 2012. QuickChecking poolboy for fun and profit; http:\/\/basho.com\/posts\/technical\/quickchecking-poolboy-for-fun-and-profit\/.  Thompson A. 2012. QuickChecking poolboy for fun and profit; http:\/\/basho.com\/posts\/technical\/quickchecking-poolboy-for-fun-and-profit\/."},{"key":"e_1_2_1_14_1","unstructured":"Yang J. Chen T. Wu M. Xu Z. Liu X. Lin H. Yang M. Long F. Zhang L. Zhou L. 2009. MODIST: transparent model checking of unmodified distributed systems; https:\/\/www.usenix.org\/legacy\/events\/nsdi09\/tech\/full_papers\/yang\/yang_html\/index.html.   Yang J. Chen T. Wu M. Xu Z. Liu X. Lin H. Yang M. Long F. Zhang L. Zhou L. 2009. MODIST: transparent model checking of unmodified distributed systems; https:\/\/www.usenix.org\/legacy\/events\/nsdi09\/tech\/full_papers\/yang\/yang_html\/index.html."},{"key":"e_1_2_1_15_1","unstructured":"Yuan D. Luo Y. Zhuang X. Rodrigues G. R. Zhao X. Zhang Y. Jain P. U. Stumm M. 2014. Simple testing can prevent most critical failures: an analysis of production failures in distributed data-intensive systems; https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/yuan.   Yuan D. Luo Y. Zhuang X. Rodrigues G. R. Zhao X. Zhang Y. Jain P. U. Stumm M. 2014. Simple testing can prevent most critical failures: an analysis of production failures in distributed data-intensive systems; https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/yuan."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"}],"container-title":["Queue"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2857274.2889274","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2857274.2889274","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:39:08Z","timestamp":1750221548000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2857274.2889274"}},"subtitle":["A practitioner\u2019s guide to increasing confidence in system correctness"],"short-title":[],"issued":{"date-parts":[[2015,11]]},"references-count":16,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2015,11]]}},"alternative-id":["10.1145\/2857274.2889274"],"URL":"https:\/\/doi.org\/10.1145\/2857274.2889274","relation":{},"ISSN":["1542-7730","1542-7749"],"issn-type":[{"type":"print","value":"1542-7730"},{"type":"electronic","value":"1542-7749"}],"subject":[],"published":{"date-parts":[[2015,11]]},"assertion":[{"value":"2015-12-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}