{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T18:00:54Z","timestamp":1768413654697,"version":"3.49.0"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2010,3,1]],"date-time":"2010-03-01T00:00:00Z","timestamp":1267401600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001711","name":"Swiss National Science Foundation","doi-asserted-by":"publisher","award":["FNS 200021-125140"],"award-info":[{"award-number":["FNS 200021-125140"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003475","name":"Hasler Stiftung","doi-asserted-by":"publisher","award":["2103"],"award-info":[{"award-number":["2103"]}],"id":[{"id":"10.13039\/501100003475","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Syst."],"published-print":{"date-parts":[[2010,3]]},"abstract":"<jats:p>We propose a new approach for developing and deploying distributed systems, in which nodes predict distributed consequences of their actions and use this information to detect and avoid errors. Each node continuously runs a state exploration algorithm on a recent consistent snapshot of its neighborhood and predicts possible future violations of specified safety properties. We describe a new state exploration algorithm, consequence prediction, which explores causally related chains of events that lead to property violation.<\/jats:p>\n          <jats:p>This article describes the design and implementation of this approach, termed CrystalBall. We evaluate CrystalBall on RandTree, BulletPrime, Paxos, and Chord distributed system implementations. We identified new bugs in mature Mace implementations of three systems. Furthermore, we show that if the bug is not corrected during system development, CrystalBall is effective in steering the execution away from inconsistent states at runtime.<\/jats:p>","DOI":"10.1145\/1731060.1731062","type":"journal-article","created":{"date-parts":[[2010,4,7]],"date-time":"2010-04-07T02:56:32Z","timestamp":1270608992000},"page":"1-49","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Predicting and preventing inconsistencies in deployed distributed systems"],"prefix":"10.1145","volume":"28","author":[{"given":"Maysam","family":"Yabandeh","sequence":"first","affiliation":[{"name":"Ecole Polytechnique F\u00e9d\u00e9rale de Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nikola","family":"Kne\u017eevi\u0107","sequence":"additional","affiliation":[{"name":"Ecole Polytechnique F\u00e9d\u00e9rale de Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dejan","family":"Kosti\u0107","sequence":"additional","affiliation":[{"name":"Ecole Polytechnique F\u00e9d\u00e9rale de Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[{"name":"Ecole Polytechnique F\u00e9d\u00e9rale de Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2010,8,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449776"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems.","author":"Ball T.","unstructured":"Ball , T. , Podelski , A. , and Rajamani , S. K . 2001. Boolean and cartesian abstraction for model checking C programs . In Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems. Ball, T., Podelski, A., and Rajamani, S. K. 2001. Boolean and cartesian abstraction for model checking C programs. In Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation.","author":"Barham P.","unstructured":"Barham , P. , Donnelly , A. , Isaacs , R. , and Mortier , R . 2004. Using magpie for request extraction and workload modelling . In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation. Barham, P., Donnelly, A., Isaacs, R., and Mortier, R. 2004. Using magpie for request extraction and workload modelling. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation."},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD'05)","author":"Bayazit A. A.","unstructured":"Bayazit , A. A. and Malik , S . 2005. Complementary use of runtime validation and model checking . In Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD'05) . IEEE Computer Society, Los Alamitos, CA, 1052--1059. Bayazit, A. A. and Malik, S. 2005. Complementary use of runtime validation and model checking. In Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD'05). IEEE Computer Society, Los Alamitos, CA, 1052--1059."},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the Annual IEEE Symposium on Logic in Computer Science.","author":"Burch J. R.","unstructured":"Burch , J. R. , Clarke , E. M. , McMillan , K. L. , Dill , D. L. , and Hwang , L. J . 1990. Symbolic model checking: 1020 states and beyond . In Proceedings of the Annual IEEE Symposium on Logic in Computer Science. Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., and Hwang, L. J. 1990. Symbolic model checking: 1020 states and beyond. In Proceedings of the Annual IEEE Symposium on Logic in Computer Science."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945474"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.22"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1281100.1281103"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/214451.214456"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/511334.511380"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.803066"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294274"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095810.1095824"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481870"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00722-4_8"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/949305.949314"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation.","author":"Dunagan J.","unstructured":"Dunagan , J. , Harvey , N. J. A. , Jones , M. B. , Kosti\u0107 , D. , Theimer , M. , and Wolman , A . 2004. FUSE: Lightweight guaranteed distributed failure notification . In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation. Dunagan, J., Harvey, N. J. A., Jones, M. B., Kosti\u0107, D., Theimer, M., and Wolman, A. 2004. FUSE: Lightweight guaranteed distributed failure notification. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3149.214121"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation.","author":"Fonseca R.","unstructured":"Fonseca , R. , Porter , G. , Katz , R. H. , Shenker , S. , and Stoica , I . 2007. X-Trace: A pervasive network tracing framework . In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation. Fonseca, R., Porter, G., Katz, R. H., Shenker, S., and Stoica, I. 2007. X-Trace: A pervasive network tracing framework. In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation."},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation.","author":"Geels D.","unstructured":"Geels , D. , Altekar , G. , Maniatis , P. , Roscoe , T. , and Stoica , I . 2007. Friday: Global comprehension for distributed replay . In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation. Geels, D., Altekar, G., Maniatis, P., Roscoe, T., and Stoica, I. 2007. Friday: Global comprehension for distributed replay. In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1035"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation.","author":"Jain N.","unstructured":"Jain , N. , Mahajan , P. , Kit , D. , Yalagandula , P. , Dahlin , M. , and Zhang , Y . 2008. Network imprecision: A new consistency metric for scalable monitoring . In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation. Jain, N., Mahajan, P., Kit, D., Yalagandula, P., Dahlin, M., and Zhang, Y. 2008. Network imprecision: A new consistency metric for scalable monitoring. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation."},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the International Conference on Thread Verification (TV'06)","author":"Janjua M. U.","unstructured":"Janjua , M. U. and Mycroft , A . 2006. Automatic correction to safety violations . In Proceedings of the International Conference on Thread Verification (TV'06) . Janjua, M. U. and Mycroft, A. 2006. Automatic correction to safety violations. In Proceedings of the International Conference on Thread Verification (TV'06)."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_23"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation.","author":"John J. P.","unstructured":"John , J. P. , Katz-Bassett , E. , Krishnamurthy , A. , Anderson , T. , and Venkataramani , A . 2008. Consensus routing: The internet as a distributed system . In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation. John, J. P., Katz-Bassett, E., Krishnamurthy, A., Anderson, T., and Venkataramani, A. 2008. Consensus routing: The internet as a distributed system. In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250755"},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation.","author":"Killian C. E.","unstructured":"Killian , C. E. , Anderson , J. W. , Jhala , R. , and Vahdat , A . 2007b. Life, death, and the critical transition: Finding liveness bugs in systems code . In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation. Killian, C. E., Anderson, J. W., Jhala, R., and Vahdat, A. 2007b. Life, death, and the critical transition: Finding liveness bugs in systems code. In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation."},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the USENIX Annual Technical Conference.","author":"Kosti\u0107 D.","unstructured":"Kosti\u0107 , D. , Braud , R. , Killian , C. , Vandekieft , E. , Anderson , J. W. , Snoeren , A. C. , and Vahdat , A . 2005. Maintaining high bandwidth under dynamic network conditions . In Proceedings of the USENIX Annual Technical Conference. Kosti\u0107, D., Braud, R., Killian, C., Vandekieft, E., Anderson, J. W., Snoeren, A. C., and Vahdat, A. 2005. Maintaining high bandwidth under dynamic network conditions. In Proceedings of the USENIX Annual Technical Conference."},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the USENIX Symposium on Internet Technologies and Systems.","author":"Kosti\u0107 D.","unstructured":"Kosti\u0107 , D. , Rodriguez , A. , Albrecht , J. , Bhirud , A. , and Vahdat , A . 2003. Using random subsets to build scalable network services . In Proceedings of the USENIX Symposium on Internet Technologies and Systems. Kosti\u0107, D., Rodriguez, A., Albrecht, J., Bhirud, A., and Vahdat, A. 2003. Using random subsets to build scalable network services. In Proceedings of the USENIX Symposium on Internet Technologies and Systems."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation.","author":"Liu X.","unstructured":"Liu , X. , Guo , Z. , Wang , X. , Chen , F. , Lian , X. , Tang , J. , Wu , M. , Kaashoek , M. F. , and Zhang , Z . 2008. D3S: Debugging deployed distributed systems . In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation. Liu, X., Guo, Z., Wang, X., Chen, F., Lian, X., Tang, J., Wu, M., Kaashoek, M. F., and Zhang, Z. 2008. D3S: Debugging deployed distributed systems. In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation."},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation.","author":"Liu X.","unstructured":"Liu , X. , Lin , W. , Pan , A. , and Zhang , Z . 2007. WiDS checker: Combating bugs in distributed systems . In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation. Liu, X., Lin, W., Pan, A., and Zhang, Z. 2007. WiDS checker: Combating bugs in distributed systems. In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-7315(02)00005-9"},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation.","author":"Musuvathi M.","unstructured":"Musuvathi , M. and Engler , D. R . 2004. Model checking large network protocol implementations . In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation. Musuvathi, M. and Engler, D. R. 2004. Model checking large network protocol implementations. In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/844128.844136"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation.","author":"Musuvathi M.","unstructured":"Musuvathi , M. , Qadeer , S. , Ball , T. , Basler , G. , Nainar , P. A. , and Neamtiu , I . 2008. Finding and reproducing heisenbugs in concurrent programs . In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation. Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P. A., and Neamtiu, I. 2008. Finding and reproducing heisenbugs in concurrent programs. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095810.1095829"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629591"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275517.1275519"},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation.","author":"Reynolds P.","unstructured":"Reynolds , P. , Killian , C. , Wiener , J. L. , Mogul , J. C. , Shah , M. A. , and Vahdat , A . 2006. Pip: Detecting the unexpected in distributed systems . In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation. Reynolds, P., Killian, C., Wiener, J. L., Mogul, J. C., Shah, M. A., and Vahdat, A. 2006. Pip: Detecting the unexpected in distributed systems. In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1080091.1080102"},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation.","author":"Rinard M. C.","unstructured":"Rinard , M. C. , Cadar , C. , Dumitran , D. , Roy , D. M. , Leu , T. , and Beebee , W. S . 2004. Enhancing server availability and security through failure-oblivious computing . In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation. Rinard, M. C., Cadar, C., Dumitran, D., Roy, D. M., Leu, T., and Beebee, W. S. 2004. Enhancing server availability and security through failure-oblivious computing. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation."},{"key":"e_1_2_1_49_1","volume-title":"Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation.","author":"Rodriguez A.","unstructured":"Rodriguez , A. , Killian , C. , Bhat , S. , Kosti\u0107 , D. , and Vahdat , A . 2004. MACEDON: Methodology for automatically creating, evaluating, and designing overlay networks . In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation. Rodriguez, A., Killian, C., Bhat, S., Kosti\u0107, D., and Vahdat, A. 2004. MACEDON: Methodology for automatically creating, evaluating, and designing overlay networks. In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/502034.502053"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/98163.98167"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693017_25"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1218063.1217973"},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of the USENIX Annual Technical Conference.","author":"Srinivasan S. M., K, S.","unstructured":"Srinivasan , S. M., K, S. , Andrews , C. R. , and Zhou , Y . 2004. Flashback: A lightweight extension for rollback and deterministic replay for software debugging . In Proceedings of the USENIX Annual Technical Conference. Srinivasan, S. M., K, S., Andrews, C. R., and Zhou, Y. 2004. Flashback: A lightweight extension for rollback and deterministic replay for software debugging. In Proceedings of the USENIX Annual Technical Conference."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2002.808407"},{"key":"e_1_2_1_56_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation.","author":"Vahdat A.","unstructured":"Vahdat , A. , Yocum , K. , Walsh , K. , Mahadevan , P. , Kosti\u0107 , D. , Chase , J. , and Becker , D . 2002. Scalability and accuracy in a large-scale network emulator . In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation. Vahdat, A., Yocum, K., Walsh, K., Mahadevan, P., Kosti\u0107, D., Chase, J., and Becker, D. 2002. Scalability and accuracy in a large-scale network emulator. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation."},{"key":"e_1_2_1_57_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation.","author":"Wang Y.","unstructured":"Wang , Y. , Kelly , T. , Kudlur , M. , Lafortune , S. , and Mahlke , S. A . 2008. Gadara: Dynamic deadlock avoidance for multithreaded programs . In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation. Wang, Y., Kelly, T., Kudlur, M., Lafortune, S., and Mahlke, S. A. 2008. Gadara: Dynamic deadlock avoidance for multithreaded programs. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480913"},{"key":"e_1_2_1_59_1","volume-title":"Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation.","author":"Yabandeh M.","unstructured":"Yabandeh , M. , Kne\u017eevi\u0107 , N. , Kosti\u0107 , D. , and Kuncak , V . 2009a. CrystalBall: Predicting and preventing inconsistencies in deployed distributed systems . In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation. Yabandeh, M., Kne\u017eevi\u0107, N., Kosti\u0107, D., and Kuncak, V. 2009a. CrystalBall: Predicting and preventing inconsistencies in deployed distributed systems. In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation."},{"key":"e_1_2_1_60_1","volume-title":"Proceedings of the Workshop on Hot Topics in Operating Systems.","author":"Yabandeh M.","unstructured":"Yabandeh , M. , Vasi\u0107 , N. , Kosti\u0107 , D. , and Kuncak , V . 2009b. Simplifying distributed system development . In Proceedings of the Workshop on Hot Topics in Operating Systems. Yabandeh, M., Vasi\u0107, N., Kosti\u0107, D., and Kuncak, V. 2009b. Simplifying distributed system development. In Proceedings of the Workshop on Hot Topics in Operating Systems."},{"key":"e_1_2_1_61_1","volume-title":"Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation.","author":"Yang J.","unstructured":"Yang , J. , Chen , T. , Wu , M. , Xu , Z. , Liu , X. , Lin , H. , Yang , M. , Long , F. , Zhang , L. , and Zhou , L . 2009. MODIST: Transparent model checking of unmodified distributed systems . In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation. Yang, J., Chen, T., Wu, M., Xu, Z., Liu, X., Lin, H., Yang, M., Long, F., Zhang, L., and Zhou, L. 2009. MODIST: Transparent model checking of unmodified distributed systems. In Proceedings of the ACM\/USENIX Symposium on Networked Systems Design and Implementation."},{"key":"e_1_2_1_62_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation.","author":"Yang J.","unstructured":"Yang , J. , Sar , C. , and Engler , D . 2006a. EXPLODE: A lightweight, general system for finding serious storage system errors . In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation. Yang, J., Sar, C., and Engler, D. 2006a. EXPLODE: A lightweight, general system for finding serious storage system errors. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1189256.1189259"}],"container-title":["ACM Transactions on Computer Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1731060.1731062","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1731060.1731062","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:41:27Z","timestamp":1750250487000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1731060.1731062"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,3]]},"references-count":63,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,3]]}},"alternative-id":["10.1145\/1731060.1731062"],"URL":"https:\/\/doi.org\/10.1145\/1731060.1731062","relation":{},"ISSN":["0734-2071","1557-7333"],"issn-type":[{"value":"0734-2071","type":"print"},{"value":"1557-7333","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,3]]},"assertion":[{"value":"2009-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-08-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}