{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T23:41:16Z","timestamp":1768520476411,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":63,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,10,14]],"date-time":"2017-10-14T00:00:00Z","timestamp":1507939200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1563763"],"award-info":[{"award-number":["CNS-1563763"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,10,14]]},"DOI":"10.1145\/3132747.3132776","type":"proceedings-article","created":{"date-parts":[[2017,10,12]],"date-time":"2017-10-12T12:51:09Z","timestamp":1507812669000},"page":"270-286","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":46,"title":["Verifying a high-performance crash-safe file system using a tree specification"],"prefix":"10.1145","author":[{"given":"Haogang","family":"Chen","sequence":"first","affiliation":[{"name":"Databricks"}]},{"given":"Tej","family":"Chajed","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}]},{"given":"Alex","family":"Konradi","sequence":"additional","affiliation":[{"name":"Google"}]},{"given":"Stephanie","family":"Wang","sequence":"additional","affiliation":[{"name":"Berkeley"}]},{"given":"Atalay","family":"\u0130leri","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}]},{"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}]},{"given":"M. Frans","family":"Kaashoek","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}]},{"given":"Nickolai","family":"Zeldovich","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}]}],"member":"320","published-online":{"date-parts":[[2017,10,14]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.196.1"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30482-1_32"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535847"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132779"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872406"},{"key":"e_1_3_2_2_9_1","unstructured":"N. Brown. Overlay filesystem. https:\/\/www.kernel.org\/doc\/Documentation\/filesystems\/overlayfs.txt.  N. Brown. Overlay filesystem. https:\/\/www.kernel.org\/doc\/Documentation\/filesystems\/overlayfs.txt."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522726"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522712"},{"key":"e_1_3_2_2_13_1","volume-title":"INRIA","author":"Coq","year":"2016","unstructured":"Coq development team. The Coq Proof Assistant Reference Manual, Version 8.5pl2 . INRIA , July 2016 . http:\/\/coq.inria.fr\/distrib\/current\/refman\/. Coq development team. The Coq Proof Assistant Reference Manual, Version 8.5pl2. INRIA, July 2016. http:\/\/coq.inria.fr\/distrib\/current\/refman\/."},{"key":"e_1_3_2_2_14_1","unstructured":"J. Corbet. ext4 and data loss. http:\/\/lwn.net\/Articles\/322823\/ Mar. 2009.  J. Corbet. ext4 and data loss. http:\/\/lwn.net\/Articles\/322823\/ Mar. 2009."},{"key":"e_1_3_2_2_15_1","volume-title":"Xv6, a simple Unix-like teaching operating system","author":"Cox R.","year":"2016","unstructured":"R. Cox , M. F. Kaashoek , and R. T. Morris . Xv6, a simple Unix-like teaching operating system , 2016 . http:\/\/pdos.csail.mit.edu\/6.828\/xv6. R. Cox, M. F. Kaashoek, and R. T. Morris. Xv6, a simple Unix-like teaching operating system, 2016. http:\/\/pdos.csail.mit.edu\/6.828\/xv6."},{"key":"e_1_3_2_2_16_1","volume-title":"Apr.","author":"Czerner L.","year":"2015","unstructured":"L. Czerner . {PATCH} ext4 : Fix data corruption caused by unwritten and delayed extents. https:\/\/lwn.net\/Articles\/645722 , Apr. 2015 . L. Czerner. {PATCH} ext4: Fix data corruption caused by unwritten and delayed extents. https:\/\/lwn.net\/Articles\/645722, Apr. 2015."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54108-7_13"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10452-7_11"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2008.35"},{"key":"e_1_3_2_2_20_1","first-page":"49","volume-title":"Proceedings of the 1st Symposium on Operating Systems Design and Implementation (OSDI)","author":"Ganger G. R.","year":"1994","unstructured":"G. R. Ganger and Y. N. Patt . Metadata update performance in file systems . In Proceedings of the 1st Symposium on Operating Systems Design and Implementation (OSDI) , pages 49 -- 60 , Monterey, CA , Nov. 1994 . G. R. Ganger and Y. N. Patt. Metadata update performance in file systems. In Proceedings of the 1st Symposium on Operating Systems Design and Implementation (OSDI), pages 49--60, Monterey, CA, Nov. 1994."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_10"},{"key":"e_1_3_2_2_22_1","volume-title":"Jan.","author":"B. Gribincea","year":"2009","unstructured":"B. Gribincea et al. Ext4 data loss. https:\/\/bugs.launchpad.net\/ubuntu\/+source\/linux\/+bug\/317781 , Jan. 2009 . B. Gribincea et al. Ext4 data loss. https:\/\/bugs.launchpad.net\/ubuntu\/+source\/linux\/+bug\/317781, Jan. 2009."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.12.018"},{"key":"e_1_3_2_2_25_1","volume-title":"April","author":"Hutchings B.","year":"2016","unstructured":"B. Hutchings . { PATCH 3.2 027\/115} jbd2 : fix fs corruption possibility in jbd2_journal_destroy() on umount path. https:\/\/lkml.org\/lkml\/2016\/4\/26\/1230 , April 2016 . B. Hutchings. {PATCH 3.2 027\/115} jbd2: fix fs corruption possibility in jbd2_journal_destroy() on umount path. https:\/\/lkml.org\/lkml\/2016\/4\/26\/1230, April 2016."},{"key":"e_1_3_2_2_26_1","volume-title":"The Open Group base specifications issue 7","author":"IEEE (The Institute of Electrical and Electronics Engineers) and The Open Group.","year":"2013","unstructured":"IEEE (The Institute of Electrical and Electronics Engineers) and The Open Group. The Open Group base specifications issue 7 , 2013 edition ( POSIX. 1-2008\/Cor 1-2013), Apr. 2013. IEEE (The Institute of Electrical and Electronics Engineers) and The Open Group. The Open Group base specifications issue 7, 2013 edition (POSIX.1-2008\/Cor 1-2013), Apr. 2013."},{"key":"e_1_3_2_2_27_1","volume-title":"Trinity: A Linux system call fuzz tester","author":"Jones D.","year":"2014","unstructured":"D. Jones . Trinity: A Linux system call fuzz tester , 2014 . http:\/\/codemonkey.org.uk\/projects\/trinity\/. D. Jones. Trinity: A Linux system call fuzz tester, 2014. http:\/\/codemonkey.org.uk\/projects\/trinity\/."},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0022-3"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87603-8_23"},{"key":"e_1_3_2_2_30_1","unstructured":"J. Kara. {PATCH} ext4: Forbid journal_async_commit in data=ordered mode. http:\/\/permalink.gmane.org\/gmane.comp.file-systems.ext4\/46977 Nov. 2014.  J. Kara. {PATCH} ext4: Forbid journal_async_commit in data=ordered mode. http:\/\/permalink.gmane.org\/gmane.comp.file-systems.ext4\/46977 Nov. 2014."},{"key":"e_1_3_2_2_31_1","unstructured":"J. Kara. ext4: fix crashes in dioread_nolock mode. http:\/\/permalink.gmane.org\/gmane.linux.kernel.commits.head\/575311 Feb. 2016.  J. Kara. ext4: fix crashes in dioread_nolock mode. http:\/\/permalink.gmane.org\/gmane.linux.kernel.commits.head\/575311 Feb. 2016."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837648"},{"key":"e_1_3_2_2_33_1","volume-title":"Ext4 filesystem","author":"Developers Linux Kernel","year":"2017","unstructured":"Linux Kernel Developers . Ext4 filesystem , 2017 . https:\/\/www.kernel.org\/doc\/Documentation\/filesystems\/ext4.txt. Linux Kernel Developers. Ext4 filesystem, 2017. https:\/\/www.kernel.org\/doc\/Documentation\/filesystems\/ext4.txt."},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/2591272.2591276"},{"key":"e_1_3_2_2_35_1","volume-title":"Proceedings of the 11th Symposium on Networked Systems Design and Implementation (NSDI)","author":"Mickens J.","year":"2014","unstructured":"J. Mickens , E. Nightingale , J. Elson , B. Fan , A. Kadav , V. Chidambaram , O. Khan , K. Nareddy , and D. Gehring . Blizzard: Fast, cloud-scale block storage for cloud-oblivious applications . In Proceedings of the 11th Symposium on Networked Systems Design and Implementation (NSDI) , Seattle, WA , Apr. 2014 . J. Mickens, E. Nightingale, J. Elson, B. Fan, A. Kadav, V. Chidambaram, O. Khan, K. Nareddy, and D. Gehring. Blizzard: Fast, cloud-scale block storage for cloud-oblivious applications. In Proceedings of the 11th Symposium on Networked Systems Design and Implementation (NSDI), Seattle, WA, Apr. 2014."},{"key":"e_1_3_2_2_36_1","volume-title":"Sept.","author":"Mostafa K.","year":"2014","unstructured":"K. Mostafa . { PATCH 3.13 075\/103} jbd2 : fix descriptor block size handling errors with journal_csum. https:\/\/lkml.org\/lkml\/2014\/9\/30\/747 , Sept. 2014 . K. Mostafa. {PATCH 3.13 075\/103} jbd2: fix descriptor block size handling errors with journal_csum. https:\/\/lkml.org\/lkml\/2014\/9\/30\/747, Sept. 2014."},{"key":"e_1_3_2_2_37_1","volume-title":"June","author":"Mostafa K.","year":"2016","unstructured":"K. Mostafa . ext4 : fix null pointer dereference when journal restart fails. https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=9d506594069355d1fb2de3f9104667312ff08ed3 , June 2016 . K. Mostafa. ext4: fix null pointer dereference when journal restart fails. https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=9d506594069355d1fb2de3f9104667312ff08ed3, June 2016."},{"key":"e_1_3_2_2_38_1","first-page":"787","volume-title":"Proceedings of the 2017 USENIX Annual Technical Conference","author":"Park D.","year":"2017","unstructured":"D. Park and D. Shin . iJournaling: Fine-grained journaling for improving the latency of fsync system call . In Proceedings of the 2017 USENIX Annual Technical Conference , pages 787 -- 798 , Santa Clara, CA , July 2017 . D. Park and D. Shin. iJournaling: Fine-grained journaling for improving the latency of fsync system call. In Proceedings of the 2017 USENIX Annual Technical Conference, pages 787--798, Santa Clara, CA, July 2017."},{"key":"e_1_3_2_2_39_1","volume-title":"Python implementation of TPC-C","author":"Pavlo A.","year":"2017","unstructured":"A. Pavlo . Python implementation of TPC-C , 2017 . https:\/\/github.com\/apavlo\/py-tpcc. A. Pavlo. Python implementation of TPC-C, 2017. https:\/\/github.com\/apavlo\/py-tpcc."},{"key":"e_1_3_2_2_40_1","first-page":"433","volume-title":"Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Pillai T. S.","year":"2014","unstructured":"T. S. Pillai , V. Chidambaram , R. Alagappan , S. Al-Kiswany , A. C. Arpaci-Dusseau , and R. H. Arpaci-Dusseau . All file systems are not created equal: On the complexity of crafting crash-consistent applications . In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI) , pages 433 -- 448 , Broomfield, CO , Oct. 2014 . T. S. Pillai, V. Chidambaram, R. Alagappan, S. Al-Kiswany, A. C. Arpaci-Dusseau, and R. H. Arpaci-Dusseau. All file systems are not created equal: On the complexity of crafting crash-consistent applications. In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI), pages 433--448, Broomfield, CO, Oct. 2014."},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/3129633.3129650"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815411"},{"key":"e_1_3_2_2_44_1","volume-title":"Necessary step(s) to synchronize filename operations on disk","author":"Roche X.","year":"2013","unstructured":"X. Roche , G. Clare , K. Schwarz , P. Eggert , J. Schilling , A. Josey , and J. Pugsley . Necessary step(s) to synchronize filename operations on disk . Austin Group Defect Tracker , Mar. 2013 . http:\/\/austingroupbugs.net\/view.php?id=672. X. Roche, G. Clare, K. Schwarz, P. Eggert, J. Schilling, A. Josey, and J. Pugsley. Necessary step(s) to synchronize filename operations on disk. Austin Group Defect Tracker, Mar. 2013. http:\/\/austingroupbugs.net\/view.php?id=672."},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/121132.121137"},{"key":"e_1_3_2_2_46_1","unstructured":"E. Sandeen. {PATCH} ext4: fix unjournaled inode bitmap modification. http:\/\/permalink.gmane.org\/gmane.comp.file-systems.ext4\/35119 Oct. 2012.  E. Sandeen. {PATCH} ext4: fix unjournaled inode bitmap modification. http:\/\/permalink.gmane.org\/gmane.comp.file-systems.ext4\/35119 Oct. 2012."},{"key":"e_1_3_2_2_47_1","volume-title":"Mar.","author":"Sigurbjarnarson H.","year":"2017","unstructured":"H. Sigurbjarnarson and X. Wang . Personal communication , Mar. 2017 . H. Sigurbjarnarson and X. Wang. Personal communication, Mar. 2017."},{"key":"e_1_3_2_2_48_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_2_49_1","volume-title":"The Yggdrasil toolkit","author":"Sigurbjarnarson H.","year":"2017","unstructured":"H. Sigurbjarnarson , J. Bornholt , E. Torlak , and X. Wang . The Yggdrasil toolkit , 2017 . https:\/\/github.com\/locore\/yggdrasil\/. H. Sigurbjarnarson, J. Bornholt, E. Torlak, and X. Wang. The Yggdrasil toolkit, 2017. https:\/\/github.com\/locore\/yggdrasil\/."},{"key":"e_1_3_2_2_50_1","volume-title":"Oct.","author":"Szeredi M.","year":"2016","unstructured":"M. Szeredi . ovl: fsync after copy-up. https:\/\/github.com\/torvalds\/linux\/commit\/641089c1549d8d3df0b047b5de7e9a111362cdce , Oct. 2016 . M. Szeredi. ovl: fsync after copy-up. https:\/\/github.com\/torvalds\/linux\/commit\/641089c1549d8d3df0b047b5de7e9a111362cdce, Oct. 2016."},{"key":"e_1_3_2_2_51_1","volume-title":"fdatasync(2): Linux man page","author":"The Linux","year":"2017","unstructured":"The Linux man-pages project. fdatasync(2): Linux man page , 2017 . http:\/\/man7.org\/linux\/man-pages\/man2\/fdatasync.2.html. The Linux man-pages project. fdatasync(2): Linux man page, 2017. http:\/\/man7.org\/linux\/man-pages\/man2\/fdatasync.2.html."},{"key":"e_1_3_2_2_52_1","volume-title":"fdatasync: synchronize the data of a file","author":"The Open Group","year":"2016","unstructured":"The Open Group . fdatasync: synchronize the data of a file , 2016 . http:\/\/pubs.opengroup.org\/onlinepubs\/9699919799\/functions\/fdatasync.html. The Open Group. fdatasync: synchronize the data of a file, 2016. http:\/\/pubs.opengroup.org\/onlinepubs\/9699919799\/functions\/fdatasync.html."},{"key":"e_1_3_2_2_53_1","unstructured":"T. Ts'o. {PATCH} ext4 jbd2: add REQ_FUA flag when recording an error flag. http:\/\/permalink.gmane.org\/gmane.comp.file-systems.ext4\/49323 July 2015.  T. Ts'o. {PATCH} ext4 jbd2: add REQ_FUA flag when recording an error flag. http:\/\/permalink.gmane.org\/gmane.comp.file-systems.ext4\/49323 July 2015."},{"key":"e_1_3_2_2_54_1","volume-title":"Oct.","author":"Ts'o T.","year":"2015","unstructured":"T. Ts'o . {PATCH} ext4 : use private version of page_zero_new_buffers() for data=journal mode. https:\/\/lkml.org\/lkml\/2015\/10\/9\/1 , Oct. 2015 . T. Ts'o. {PATCH} ext4: use private version of page_zero_new_buffers() for data=journal mode. https:\/\/lkml.org\/lkml\/2015\/10\/9\/1, Oct. 2015."},{"key":"e_1_3_2_2_55_1","volume-title":"June","author":"Ts'o T.","year":"2015","unstructured":"T. Ts'o . ext4: fix race between truncate and __ext4_journalled_writepage(). https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=bdf96838aea6a265f2ae6cbcfb12a778c84a0b8e , June 2015 . T. Ts'o. ext4: fix race between truncate and __ext4_journalled_writepage(). https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=bdf96838aea6a265f2ae6cbcfb12a778c84a0b8e, June 2015."},{"key":"e_1_3_2_2_56_1","volume-title":"Proceedings of the 4th Annual LinuxExpo","author":"Tweedie S. C.","year":"1998","unstructured":"S. C. Tweedie . Journaling the Linux ext2fs filesystem . In Proceedings of the 4th Annual LinuxExpo , Durham, NC , May 1998 . S. C. Tweedie. Journaling the Linux ext2fs filesystem. In Proceedings of the 4th Annual LinuxExpo, Durham, NC, May 1998."},{"key":"e_1_3_2_2_57_1","volume-title":"Certifying checksum-based logging in the RapidFSCQ crash-safe filesystem. Master's thesis","author":"Wang S.","year":"2016","unstructured":"S. Wang . Certifying checksum-based logging in the RapidFSCQ crash-safe filesystem. Master's thesis , Massachusetts Institute of Technology , June 2016 . S. Wang. Certifying checksum-based logging in the RapidFSCQ crash-safe filesystem. Master's thesis, Massachusetts Institute of Technology, June 2016."},{"key":"e_1_3_2_2_58_1","unstructured":"M. Wenzel. Some aspects of Unix file-system security Aug. 2014. http:\/\/isabelle.in.tum.de\/library\/HOL\/HOL-Unix\/Unix.html.  M. Wenzel. Some aspects of Unix file-system security Aug. 2014. http:\/\/isabelle.in.tum.de\/library\/HOL\/HOL-Unix\/Unix.html."},{"key":"e_1_3_2_2_59_1","unstructured":"D. J. Wong. jbd2: Fix endian mixing problems in the checksumming code. http:\/\/lists.openwall.net\/linux-ext4\/2013\/07\/17\/1 July 2013.  D. J. Wong. jbd2: Fix endian mixing problems in the checksumming code. http:\/\/lists.openwall.net\/linux-ext4\/2013\/07\/17\/1 July 2013."},{"key":"e_1_3_2_2_60_1","unstructured":"D. J. Wong. {PATCH} ext4: fix same-dir rename when inline data directory overflows. http:\/\/permalink.gmane.org\/gmane.comp.file-systems.ext4\/45594 Aug. 2014.  D. J. Wong. {PATCH} ext4: fix same-dir rename when inline data directory overflows. http:\/\/permalink.gmane.org\/gmane.comp.file-systems.ext4\/45594 Aug. 2014."},{"key":"e_1_3_2_2_61_1","first-page":"323","volume-title":"Proceedings of the 14th USENIX Conference on File and Storage Technologies (FAST)","author":"Xu J.","year":"2016","unstructured":"J. Xu and S. Swanson . NOVA: A log-structured file system for hybrid volatile\/non-volatile main memories . In Proceedings of the 14th USENIX Conference on File and Storage Technologies (FAST) , pages 323 -- 338 , Santa Clara, CA , Feb. 2016 . J. Xu and S. Swanson. NOVA: A log-structured file system for hybrid volatile\/non-volatile main memories. In Proceedings of the 14th USENIX Conference on File and Storage Technologies (FAST), pages 323--338, Santa Clara, CA, Feb. 2016."},{"key":"e_1_3_2_2_62_1","first-page":"273","volume-title":"Proceedings of the 6th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Yang J.","year":"2004","unstructured":"J. Yang , P. Twohey , D. Engler , and M. Musuvathi . Using model checking to find serious file system errors . In Proceedings of the 6th Symposium on Operating Systems Design and Implementation (OSDI) , pages 273 -- 287 , San Francisco, CA , Dec. 2004 . J. Yang, P. Twohey, D. Engler, and M. Musuvathi. Using model checking to find serious file system errors. In Proceedings of the 6th Symposium on Operating Systems Design and Implementation (OSDI), pages 273--287, San Francisco, CA, Dec. 2004."},{"key":"e_1_3_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.7"},{"key":"e_1_3_2_2_64_1","first-page":"131","volume-title":"Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Yang J.","year":"2006","unstructured":"J. Yang , P. Twohey , D. Engler , and M. Musuvathi . eXplode: A lightweight, general system for finding serious storage system errors . In Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI) , pages 131 -- 146 , Seattle, WA , Nov. 2006 . J. Yang, P. Twohey, D. Engler, and M. Musuvathi. eXplode: A lightweight, general system for finding serious storage system errors. In Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI), pages 131--146, Seattle, WA, Nov. 2006."},{"key":"e_1_3_2_2_65_1","first-page":"449","volume-title":"Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Zheng M.","year":"2014","unstructured":"M. Zheng , J. Tucek , D. Huang , F. Qin , M. Lillibridge , E. S. Yang , B. W. Zhao , and S. Singh . Torturing databases for fun and profit . In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI) , pages 449 -- 464 , Broomfield, CO , Oct. 2014 . M. Zheng, J. Tucek, D. Huang, F. Qin, M. Lillibridge, E. S. Yang, B. W. Zhao, and S. Singh. Torturing databases for fun and profit. In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI), pages 449--464, Broomfield, CO, Oct. 2014."}],"event":{"name":"SOSP '17: ACM SIGOPS 26th Symposium on Operating Systems Principles","location":"Shanghai China","acronym":"SOSP '17","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX Assoc USENIX Assoc"]},"container-title":["Proceedings of the 26th Symposium on Operating Systems Principles"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3132747.3132776","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3132747.3132776","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:10:57Z","timestamp":1750212657000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3132747.3132776"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,14]]},"references-count":63,"alternative-id":["10.1145\/3132747.3132776","10.1145\/3132747"],"URL":"https:\/\/doi.org\/10.1145\/3132747.3132776","relation":{},"subject":[],"published":{"date-parts":[[2017,10,14]]},"assertion":[{"value":"2017-10-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}