{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:35Z","timestamp":1781238935614,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":67,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,10,4]],"date-time":"2015-10-04T00:00:00Z","timestamp":1443916800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NSF CCF","award":["CCF-1253229"],"award-info":[{"award-number":["CCF-1253229"]}]},{"name":"NSF CNS","award":["CNS-1053143"],"award-info":[{"award-number":["CNS-1053143"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,10,4]]},"DOI":"10.1145\/2815400.2815402","type":"proceedings-article","created":{"date-parts":[[2015,10,1]],"date-time":"2015-10-01T12:01:58Z","timestamp":1443700918000},"page":"18-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":165,"title":["Using Crash Hoare logic for certifying the FSCQ file system"],"prefix":"10.1145","author":[{"given":"Haogang","family":"Chen","sequence":"first","affiliation":[{"name":"MIT CSAIL"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"Ziegler","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tej","family":"Chajed","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"M. Frans","family":"Kaashoek","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nickolai","family":"Zeldovich","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2015,10,4]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Proceedings of the 15th Workshop on Hot Topics in Operating Systems (HotOS)","author":"Alagappan R.","year":"2015","unstructured":"R. Alagappan , V. Chidambaram , T. S. Pillai , A. C. Arpaci-Dusseau , and R. H. Arpaci-Dusseau . Beyond Storage Apis: Provable Semantics For Storage Stacks . In Proceedings of the 15th Workshop on Hot Topics in Operating Systems (HotOS) , Kartause Ittingen, Switzerland , May 2015 . R. Alagappan, V. Chidambaram, T. S. Pillai, A. C. Arpaci-Dusseau, and R. H. Arpaci-Dusseau. Beyond Storage Apis: Provable Semantics For Storage Stacks. In Proceedings of the 15th Workshop on Hot Topics in Operating Systems (HotOS), Kartause Ittingen, Switzerland, May 2015."},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISoLA.2006.14"},{"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","volume-title":"Operating Systems: Three Easy Pieces","author":"Arpaci-Dusseau R. H.","year":"2014","unstructured":"R. H. Arpaci-Dusseau and A. C. Arpaci-Dusseau . Operating Systems: Three Easy Pieces . Arpaci-Dusseau Books , May 2014 . R. H. Arpaci-Dusseau and A. C. Arpaci-Dusseau. Operating Systems: Three Easy Pieces. Arpaci-Dusseau Books, May 2014."},{"key":"e_1_3_2_2_7_1","volume-title":"Haskell bindings for the FUSE library","author":"Bobbio J.","year":"2014","unstructured":"J. Bobbio Haskell bindings for the FUSE library , 2014 . https:\/\/github.com\/m15k\/hfuse. J. Bobbio et al. Haskell bindings for the FUSE library, 2014. https:\/\/github.com\/m15k\/hfuse."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509546"},{"key":"e_1_3_2_2_9_1","volume-title":"Proceedings of the 15th Workshop on Hot Topics in Operating Systems (HotOS)","author":"Chen H.","year":"2015","unstructured":"H. Chen , D. Ziegler , A. Chlipala , M. F. Kaashoek , E. Kohler , and N. Zeldovich . Specifying crash safety for storage systems . In Proceedings of the 15th Workshop on Hot Topics in Operating Systems (HotOS) , Kartause Ittingen, Switzerland , May 2015 . H. Chen, D. Ziegler, A. Chlipala, M. F. Kaashoek, E. Kohler, and N. Zeldovich. Specifying crash safety for storage systems. In Proceedings of the 15th Workshop on Hot Topics in Operating Systems (HotOS), Kartause Ittingen, Switzerland, May 2015."},{"key":"e_1_3_2_2_10_1","volume-title":"May","author":"Chinner D.","year":"2014","unstructured":"D. Chinner . xfs: xfs_dir_fsync() returns positive errno , May 2014 . https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=43ec1460a2189fbee87980dd3d3e64cba2f11e1f. D. Chinner. xfs: xfs_dir_fsync() returns positive errno, May 2014. https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=43ec1460a2189fbee87980dd3d3e64cba2f11e1f."},{"key":"e_1_3_2_2_11_1","volume-title":"Sept.","author":"Chinner D.","year":"2014","unstructured":"D. Chinner . xfs: fix double free in xlog_recover_commit_trans , Sept. 2014 . http:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=88b863db97a18a04c90ebd57d84e1b7863114dcb. D. Chinner. xfs: fix double free in xlog_recover_commit_trans, Sept. 2014. http:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=88b863db97a18a04c90ebd57d84e1b7863114dcb."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500592"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522712"},{"key":"e_1_3_2_2_15_1","volume-title":"INRIA","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_2_16_1","volume-title":"Xv6, a simple Unix-like teaching operating system","author":"Cox R.","year":"2014","unstructured":"R. Cox , M. F. Kaashoek , and R. T. Morris . Xv6, a simple Unix-like teaching operating system , 2014 . http:\/\/pdos.csail.mit.edu\/6.828\/2014\/xv6.html. R. Cox, M. F. Kaashoek, and R. T. Morris. Xv6, a simple Unix-like teaching operating system, 2014. http:\/\/pdos.csail.mit.edu\/6.828\/2014\/xv6.html."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/949305.949314"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_3_2_2_19_1","volume-title":"Proceedings of the 5th Working Conference on Verified Software: Theories, Tools and Experiments","author":"Ernst G.","year":"2013","unstructured":"G. Ernst , G. Schellhorn , D. Haneberg , J. Pf\u00e4hler , and W. Reif . Verification of a virtual filesystem switch . In Proceedings of the 5th Working Conference on Verified Software: Theories, Tools and Experiments , Menlo Park, CA , May 2013 . G. Ernst, G. Schellhorn, D. Haneberg, J. Pf\u00e4hler, and W. Reif. Verification of a virtual filesystem switch. In Proceedings of the 5th Working Conference on Verified Software: Theories, Tools and Experiments, Menlo Park, CA, May 2013."},{"key":"e_1_3_2_2_20_1","volume-title":"Proceedings of the 7th Working Conference on Verified Software: Theories, Tools and Experiments","author":"Ernst G.","year":"2015","unstructured":"G. Ernst , J. Pf\u00e4hler , G. Schellhorn , and W. Reif . Inside a verified flash file system: Transactions & garbage collection . In Proceedings of the 7th Working Conference on Verified Software: Theories, Tools and Experiments , San Francisco, CA , July 2015 . G. Ernst, J. Pf\u00e4hler, G. Schellhorn, and W. Reif. Inside a verified flash file system: Transactions & garbage collection. In Proceedings of the 7th Working Conference on Verified Software: Theories, Tools and Experiments, San Francisco, CA, July 2015."},{"key":"e_1_3_2_2_21_1","unstructured":"R. Escriva. Claiming Bitcoin's bug bounty Nov. 2013. http:\/\/hackingdistributed.com\/2013\/11\/27\/bitcoin-leveldb\/.  R. Escriva. Claiming Bitcoin's bug bounty Nov. 2013. http:\/\/hackingdistributed.com\/2013\/11\/27\/bitcoin-leveldb\/."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10452-7_11"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2008.35"},{"key":"e_1_3_2_2_24_1","volume-title":"FUSE: Filesystem in userspace","author":"FUSE.","year":"2013","unstructured":"FUSE. FUSE: Filesystem in userspace , 2013 . http:\/\/fuse.sourceforge.net\/. FUSE. FUSE: Filesystem in userspace, 2013. http:\/\/fuse.sourceforge.net\/."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_10"},{"key":"e_1_3_2_2_26_1","volume-title":"Proceedings of the 38th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN)","author":"Geambasu R.","year":"2008","unstructured":"R. Geambasu , A. Birrell , and J. MacCormick . Experiences with formal specification of fault-tolerant storage systems . In Proceedings of the 38th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN) , Anchorage, AK , June 2008 . R. Geambasu, A. Birrell, and J. MacCormick. Experiences with formal specification of fault-tolerant storage systems. In Proceedings of the 38th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN), Anchorage, AK, June 2008."},{"key":"e_1_3_2_2_27_1","volume-title":"Mar.","author":"Goldstein A.","year":"2011","unstructured":"A. Goldstein . ext4 : handle errors in ext4_rename , Mar. 2011 . https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=ef6078930263bfcdcfe4dddb2cd85254b4cf4f5c. A. Goldstein. ext4: handle errors in ext4_rename, Mar. 2011. https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=ef6078930263bfcdcfe4dddb2cd85254b4cf4f5c."},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_3_2_2_29_1","first-page":"131","volume-title":"Proceedings of the 8th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Gunawi H. S.","year":"2008","unstructured":"H. S. Gunawi , A. Rajimwale , A. C. Arpaci-Dusseau , and R. H. Arpaci-Dusseau . SQCK: A declarative file system checker . In Proceedings of the 8th Symposium on Operating Systems Design and Implementation (OSDI) , pages 131 -- 146 , San Diego, CA , Dec. 2008 . H. S. Gunawi, A. Rajimwale, A. C. Arpaci-Dusseau, and R. H. Arpaci-Dusseau. SQCK: A declarative file system checker. In Proceedings of the 8th Symposium on Operating Systems Design and Implementation (OSDI), pages 131--146, San Diego, CA, Dec. 2008."},{"key":"e_1_3_2_2_30_1","first-page":"165","volume-title":"Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Hawblitzel C.","year":"2014","unstructured":"C. Hawblitzel , J. Howell , J. R. Lorch , A. Narayan , B. Parno , D. Zhang , and B. Zill . Ironclad Apps: End-to-end security via automated full-system verification . In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI) , pages 165 -- 181 , Broomfield, CO , Oct. 2014 . C. Hawblitzel, J. Howell, J. R. Lorch, A. Narayan, B. Parno, D. Zhang, and B. Zill. Ironclad Apps: End-to-end security via automated full-system verification. In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI), pages 165--181, Broomfield, CO, Oct. 2014."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.12.018"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_2_34_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_35_1","volume-title":"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_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0022-3"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87603-8_23"},{"key":"e_1_3_2_2_38_1","volume-title":"July","author":"Kara J.","year":"2010","unstructured":"J. Kara . ext3 : Avoid filesystem corruption after a crash under heavy delete load , July 2010 . https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=f25f624263445785b94f39739a6339ba9ed3275d. J. Kara. ext3: Avoid filesystem corruption after a crash under heavy delete load, July 2010. https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=f25f624263445785b94f39739a6339ba9ed3275d."},{"key":"e_1_3_2_2_39_1","volume-title":"Mar.","author":"Kara J.","year":"2012","unstructured":"J. Kara . jbd2: issue cache flush after checkpointing even with internal journal , Mar. 2012 . http:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=79feb521a44705262d15cc819a4117a447b11ea7. J. Kara. jbd2: issue cache flush after checkpointing even with internal journal, Mar. 2012. http:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=79feb521a44705262d15cc819a4117a447b11ea7."},{"key":"e_1_3_2_2_40_1","volume-title":"Oct.","author":"Kara J.","year":"2014","unstructured":"J. Kara . ext4: fix overflow when updating superblock backups after resize , Oct. 2014 . http:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=9378c6768e4fca48971e7b6a9075bc006eda981d. J. Kara. ext4: fix overflow when updating superblock backups after resize, Oct. 2014. http:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=9378c6768e4fca48971e7b6a9075bc006eda981d."},{"key":"e_1_3_2_2_41_1","volume-title":"Trustworthy file systems","author":"Keller G.","year":"2014","unstructured":"G. Keller . Trustworthy file systems , 2014 . http:\/\/www.ssrg.nicta.com.au\/projects\/TS\/filesystems.pml. G. Keller. Trustworthy file systems, 2014. http:\/\/www.ssrg.nicta.com.au\/projects\/TS\/filesystems.pml."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2525528.2525530"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/2591272.2591276"},{"key":"e_1_3_2_2_48_1","volume-title":"Dec.","author":"Manana F.","year":"2014","unstructured":"F. Manana . Btrfs : fix race between writing free space cache and trimming , Dec. 2014 . http:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=55507ce3612365a5173dfb080a4baf45d1ef8cd1. F. Manana. Btrfs: fix race between writing free space cache and trimming, Dec. 2014. http:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=55507ce3612365a5173dfb080a4baf45d1ef8cd1."},{"key":"e_1_3_2_2_49_1","volume-title":"Nov.","author":"Mason C.","year":"2008","unstructured":"C. Mason . Btrfs : prevent loops in the directory tree when creating snapshots , Nov. 2008 . http:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=ea9e8b11bd1252dcbc23afefcf1a52ec6aa3c113. C. Mason. Btrfs: prevent loops in the directory tree when creating snapshots, Nov. 2008. http:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=ea9e8b11bd1252dcbc23afefcf1a52ec6aa3c113."},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/128765.128770"},{"key":"e_1_3_2_2_51_1","unstructured":"A. Morton. {PATCH} ext2\/ext3 -ENOSPC bug Mar. 2004. https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/tglx\/history.git\/commit\/?id=5e9087ad3928c9d80cc62b583c3034f864b6d315.  A. Morton. {PATCH} ext2\/ext3 -ENOSPC bug Mar. 2004. https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/tglx\/history.git\/commit\/?id=5e9087ad3928c9d80cc62b583c3034f864b6d315."},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26529-2_10"},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250741"},{"key":"e_1_3_2_2_55_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_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/121132.121137"},{"key":"e_1_3_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_2"},{"key":"e_1_3_2_2_59_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_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159809"},{"key":"e_1_3_2_2_61_1","first-page":"33","volume-title":"Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Wang X.","year":"2014","unstructured":"X. Wang , D. Lazar , N. Zeldovich , A. Chlipala , and Z. Tatlock . Jitk: A trustworthy in-kernel interpreter infrastructure . In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI) , pages 33 -- 47 , Broomfield, CO , Oct. 2014 . X. Wang, D. Lazar, N. Zeldovich, A. Chlipala, and Z. Tatlock. Jitk: A trustworthy in-kernel interpreter infrastructure. In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI), pages 33--47, Broomfield, CO, Oct. 2014."},{"key":"e_1_3_2_2_62_1","volume-title":"Aug.","author":"Wenzel M.","year":"2014","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_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_2_64_1","volume-title":"Aug.","author":"Wong D. J.","year":"2014","unstructured":"D. J. Wong . ext4: fix same-dir rename when inline data directory overflows , Aug. 2014 . https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=d80d448c6c5bdd32605b78a60fe8081d82d4da0f. D. J. Wong. ext4: fix same-dir rename when inline data directory overflows, Aug. 2014. https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=d80d448c6c5bdd32605b78a60fe8081d82d4da0f."},{"key":"e_1_3_2_2_65_1","volume-title":"June","author":"Xie M.","year":"2014","unstructured":"M. Xie . Btrfs: fix broken free space cache after the system crashed , June 2014 . https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=e570fd27f2c5d7eac3876bccf99e9838d7f911a3. M. Xie. Btrfs: fix broken free space cache after the system crashed, June 2014. https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/stable\/linux-stable.git\/commit\/?id=e570fd27f2c5d7eac3876bccf99e9838d7f911a3."},{"key":"e_1_3_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806610"},{"key":"e_1_3_2_2_67_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_68_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.7"},{"key":"e_1_3_2_2_69_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_70_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 '15: ACM SIGOPS 25th Symposium on Operating Systems Principles","location":"Monterey California","acronym":"SOSP '15","sponsor":["SSRC Storage Systems Research Center, UC Santa Cruz","SIGOPS ACM Special Interest Group on Operating Systems"]},"container-title":["Proceedings of the 25th Symposium on Operating Systems Principles"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2815400.2815402","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2815400.2815402","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:38Z","timestamp":1750225718000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2815400.2815402"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,10,4]]},"references-count":67,"alternative-id":["10.1145\/2815400.2815402","10.1145\/2815400"],"URL":"https:\/\/doi.org\/10.1145\/2815400.2815402","relation":{},"subject":[],"published":{"date-parts":[[2015,10,4]]},"assertion":[{"value":"2015-10-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}