{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T03:28:55Z","timestamp":1792726135919,"version":"4.5.0"},"publisher-location":"New York, NY, USA","reference-count":59,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,4,23]],"date-time":"2017-04-23T00:00:00Z","timestamp":1492905600000},"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":[],"published-print":{"date-parts":[[2017,4,23]]},"DOI":"10.1145\/3064176.3064183","type":"proceedings-article","created":{"date-parts":[[2017,4,17]],"date-time":"2017-04-17T12:27:04Z","timestamp":1492432024000},"page":"328-343","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":57,"title":["An Empirical Study on the Correctness of Formally Verified Distributed Systems"],"prefix":"10.1145","author":[{"given":"Pedro","family":"Fonseca","sequence":"first","affiliation":[{"name":"University of Washington"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kaiyuan","family":"Zhang","sequence":"additional","affiliation":[{"name":"University of Washington"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xi","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Washington"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Arvind","family":"Krishnamurthy","sequence":"additional","affiliation":[{"name":"University of Washington"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,4,23]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784241"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"e_1_3_2_1_4_1","first-page":"364","volume-title":"Formal methods for Components and Objects","author":"Barnett M.","year":"2005","unstructured":"M. Barnett , B.-Y. E. Chang , R. DeLine , B. Jacobs , and K. R. M. Leino . Boogie: A modular reusable verifier for object-oriented programs . In Formal methods for Components and Objects , pages 364 -- 387 . Springer , 2005 . M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Formal methods for Components and Objects, pages 364--387. Springer, 2005."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2080.357392"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180445"},{"key":"e_1_3_2_1_7_1","first-page":"209","volume-title":"Proceedings of the 8th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Cadar C.","year":"2008","unstructured":"C. Cadar , D. Dunbar , and D. Engler . KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs . In Proceedings of the 8th Symposium on Operating Systems Design and Implementation (OSDI) , pages 209 -- 224 , San Diego, CA , Dec. 2008 . C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th Symposium on Operating Systems Design and Implementation (OSDI), pages 209--224, San Diego, CA, Dec. 2008."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594301"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737955"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/296806.296824"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103799.2103805"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/502034.502042"},{"key":"e_1_3_2_1_14_1","volume-title":"INRIA","author":"Coq","year":"2014","unstructured":"Coq development team. Coq Reference Manual, Version 8.4pl5 . INRIA , Oct. 2014 . http:\/\/coq.inria.fr\/distrib\/current\/refman\/. Coq development team. Coq Reference Manual, Version 8.4pl5. INRIA, Oct. 2014. http:\/\/coq.inria.fr\/distrib\/current\/refman\/."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/C-M.1978.218136"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2010.5544315"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1966445.1966465"},{"key":"e_1_3_2_1_20_1","first-page":"285312","article-title":"Using I\/O automata for developing distributed systems","volume":"13","author":"Garland S. J.","year":"2000","unstructured":"S. J. Garland and N. A. Lynch . Using I\/O automata for developing distributed systems . Foundations of Component-Based Systems , 13 : 285312 , 2000 . S. J. Garland and N. A. Lynch. Using I\/O automata for developing distributed systems. Foundations of Component-Based Systems, 13:285312, 2000.","journal-title":"Foundations of Component-Based Systems"},{"key":"e_1_3_2_1_21_1","volume-title":"Proceedings of the 14th Workshop on Hot Topics in Operating Systems (HotOS), 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 14th Workshop on Hot Topics in Operating Systems (HotOS), 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 14th Workshop on Hot Topics in Operating Systems (HotOS), Santa Ana Pueblo, NM, May 2013."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926424"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009893"},{"key":"e_1_3_2_1_27_1","first-page":"243","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 -- 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--256, Cambridge, MA, Apr. 2007."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815416"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_3_2_1_37_1","first-page":"289","volume-title":"Proceedings of the 6th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Li Z.","year":"2004","unstructured":"Z. Li , S. Lu , S. Myagmar , and Y. Zhou . CP-Miner: A tool for finding copy-paste and related bugs in operating system code . In Proceedings of the 6th Symposium on Operating Systems Design and Implementation (OSDI) , pages 289 -- 302 , San Francisco, CA , Dec. 2004 . Z. Li, S. Lu, S. Myagmar, and Y. Zhou. CP-Miner: A tool for finding copy-paste and related bugs in operating system code. In Proceedings of the 6th Symposium on Operating Systems Design and Implementation (OSDI), pages 289--302, San Francisco, CA, Dec. 2004."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/800215.806567"},{"key":"e_1_3_2_1_39_1","first-page":"423","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 . D3S: Debugging deployed distributed systems . In Proceedings of the 5th Symposium on Networked Systems Design and Implementation (NSDI) , pages 423 -- 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. D3S: Debugging deployed distributed systems. In Proceedings of the 5th Symposium on Networked Systems Design and Implementation (NSDI), pages 423--437, San Francisco, CA, Apr. 2008."},{"key":"e_1_3_2_1_40_1","first-page":"313","volume-title":"Proceedings of the 10th Symposium on Networked Systems Design and Implementation (NSDI)","author":"Lloyd W.","year":"2013","unstructured":"W. Lloyd , M. J. Freedman , M. Kaminsky , and D. G. Andersen . Stronger semantics for low-latency geo-replicated storage . In Proceedings of the 10th Symposium on Networked Systems Design and Implementation (NSDI) , pages 313 -- 328 , Lombard, IL , Apr. 2013 . W. Lloyd, M. J. Freedman, M. Kaminsky, and D. G. Andersen. Stronger semantics for low-latency geo-replicated storage. In Proceedings of the 10th Symposium on Networked Systems Design and Implementation (NSDI), pages 313--328, Lombard, IL, Apr. 2013."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/2591272.2591276"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1346281.1346323"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25942-0_19"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/238721.238781"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.84877"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/2643634.2643666"},{"issue":"4","key":"e_1_3_2_1_48_1","first-page":"340","article-title":"Predicting the location and number of faults in large software systems. Software Engineering","volume":"31","author":"Ostrand T. J.","year":"2005","unstructured":"T. J. Ostrand , E. J. Weyuker , and R. M. Bell . Predicting the location and number of faults in large software systems. Software Engineering , IEEE Transactions on , 31 ( 4 ): 340 -- 355 , 2005 . T. J. Ostrand, E. J. Weyuker, and R. M. Bell. Predicting the location and number of faults in large software systems. Software Engineering, IEEE Transactions on, 31(4):340--355, 2005.","journal-title":"IEEE Transactions on"},{"key":"e_1_3_2_1_49_1","first-page":"291","volume-title":"Proceedings of the 13th Symposium on Networked Systems Design and Implementation (NSDI)","author":"Scott C.","year":"2016","unstructured":"C. Scott , V. Brajkovic , G. Necula , A. Krishnamurthy , and S. Shenker . Minimizing faulty executions of distributed systems . In Proceedings of the 13th Symposium on Networked Systems Design and Implementation (NSDI) , pages 291 -- 309 , Santa Clara, CA , Mar. 2016 . C. Scott, V. Brajkovic, G. Necula, A. Krishnamurthy, and S. Shenker. Minimizing faulty executions of distributed systems. In Proceedings of the 13th Symposium on Networked Systems Design and Implementation (NSDI), pages 291--309, Santa Clara, CA, Mar. 2016."},{"key":"e_1_3_2_1_50_1","first-page":"1","volume-title":"Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Sigurbjarnarson H.","year":"2016","unstructured":"H. Sigurbjarnarson , J. Bornholt , E. Torlak , and X. Wang . Push-button verification of file systems via crash refinement . In Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI) , pages 1 -- 16 , Savannah, GA , Nov. 2016 . H. Sigurbjarnarson, J. Bornholt, E. Torlak, and X. Wang. Push-button verification of file systems via crash refinement. In Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI), pages 1--16, Savannah, GA, Nov. 2016."},{"key":"e_1_3_2_1_51_1","first-page":"1","volume-title":"Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Sigurbjarnarson H.","year":"2016","unstructured":"H. Sigurbjarnarson , J. Bornholt , E. Torlak , and X. Wang . Push-button verification of file systems via crash refinement . In Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI) , pages 1 -- 16 , Savannah, GA , Nov. 2016 . H. Sigurbjarnarson, J. Bornholt, E. Torlak, and X. Wang. Push-button verification of file systems via crash refinement. In Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI), pages 1--16, Savannah, GA, Nov. 2016."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/FTCS.1992.243586"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/PDIS.1994.331722"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_1_55_1","first-page":"229","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\u0107 , D. Kosti\u0107 , 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 -- 244 , San Francisco, CA , Apr. 2008 . M. Yabandeh, N. Kne\u017eevi\u0107, D. Kosti\u0107, 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--244, San Francisco, CA, Apr. 2008."},{"key":"e_1_3_2_1_56_1","first-page":"213","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 . MoDist: Transparent model checking of unmodified distributed systems . In Proceedings of the 6th Symposium on Networked Systems Design and Implementation (NSDI) , pages 213 -- 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. MoDist: Transparent model checking of unmodified distributed systems. In Proceedings of the 6th Symposium on Networked Systems Design and Implementation (NSDI), pages 213--228, Boston, MA, Apr. 2009."},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_2_1_58_1","first-page":"249","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 -- 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--265, Broomfield, CO, Oct. 2014."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2185376.2185383"}],"event":{"name":"EuroSys '17: Twelfth EuroSys Conference 2017","location":"Belgrade Serbia","acronym":"EuroSys '17","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"]},"container-title":["Proceedings of the Twelfth European Conference on Computer Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3064176.3064183","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3064176.3064183","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:36:15Z","timestamp":1750217775000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3064176.3064183"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,23]]},"references-count":59,"alternative-id":["10.1145\/3064176.3064183","10.1145\/3064176"],"URL":"https:\/\/doi.org\/10.1145\/3064176.3064183","relation":{},"subject":[],"published":{"date-parts":[[2017,4,23]]},"assertion":[{"value":"2017-04-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}