{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T16:46:01Z","timestamp":1760028361000,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":50,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,7,27]],"date-time":"2021-07-27T00:00:00Z","timestamp":1627344000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CCF-1918225,CNS-1900706,CNS-1900589,CNS-1729939,CNS-1730726"],"award-info":[{"award-number":["CCF-1918225,CNS-1900706,CNS-1900589,CNS-1729939,CNS-1730726"]}],"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":[[2021,7,27]]},"DOI":"10.1145\/3465332.3470878","type":"proceedings-article","created":{"date-parts":[[2021,7,20]],"date-time":"2021-07-20T22:05:59Z","timestamp":1626818759000},"page":"103-110","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Model-Checking Support for File System Development"],"prefix":"10.1145","author":[{"given":"Wei","family":"Su","sequence":"first","affiliation":[{"name":"Stony Brook University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yifei","family":"Liu","sequence":"additional","affiliation":[{"name":"Stony Brook University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gomathi","family":"Ganesan","sequence":"additional","affiliation":[{"name":"Stony Brook University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerard","family":"Holzmann","sequence":"additional","affiliation":[{"name":"Nimble Research"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Scott","family":"Smolka","sequence":"additional","affiliation":[{"name":"Stony Brook University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Erez","family":"Zadok","sequence":"additional","affiliation":[{"name":"Stony Brook University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geoff","family":"Kuenning","sequence":"additional","affiliation":[{"name":"Harvey Mudd College"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,7,27]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Fuse-ext2 GitHub repository","author":"Akcan Alper","year":"2021","unstructured":"Alper Akcan . Fuse-ext2 GitHub repository , 2021 . https:\/\/github.com\/alperakcan\/fuse-ext2. Alper Akcan. Fuse-ext2 GitHub repository, 2021. https:\/\/github.com\/alperakcan\/fuse-ext2."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872406"},{"key":"e_1_3_2_1_4_1","first-page":"209","volume-title":"Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson R. Engler . KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs . In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI) , pages 209 -- 224 , San Diego, CA , December 2008 . Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 209--224, San Diego, CA, December 2008."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180445"},{"key":"e_1_3_2_1_6_1","volume-title":"Verifying an I\/O-concurrent file system. Master's thesis","author":"Chajed Tej","year":"2017","unstructured":"Tej Chajed . Verifying an I\/O-concurrent file system. Master's thesis , Massachusetts Institute of Technology , 2017 . Tej Chajed. Verifying an I\/O-concurrent file system. Master's thesis, Massachusetts Institute of Technology, 2017."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132776"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of the 15th Workshop on Hot Topics in Operating Systems (HotOS)","author":"Chen Haogang","year":"2015","unstructured":"Haogang Chen , Daniel Ziegler , Adam Chlipala , M. Frans Kaashoek , Eddie Kohler , and Nickolai 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 . Haogang Chen, Daniel Ziegler, Adam Chlipala, M. Frans Kaashoek, Eddie Kohler, and Nickolai 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_1_10_1","unstructured":"CRIU Community. Checkpoint\/restore in userspace (CRIU) 2021. https:\/\/criu.org\/.  CRIU Community. Checkpoint\/restore in userspace (CRIU) 2021. https:\/\/criu.org\/."},{"key":"e_1_3_2_1_11_1","unstructured":"Ext4. http:\/\/ext4.wiki.kernel.org\/.  Ext4. http:\/\/ext4.wiki.kernel.org\/."},{"volume-title":"syzkaller: Linux syscall fuzzer","year":"2021","key":"e_1_3_2_1_12_1","unstructured":"Google. syzkaller: Linux syscall fuzzer , 2021 . https:\/\/github.com\/google\/syzkaller. Google. syzkaller: Linux syscall fuzzer, 2021. https:\/\/github.com\/google\/syzkaller."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/174613.174616"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/645880.672083"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.9"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.110"},{"key":"e_1_3_2_1_19_1","first-page":"197","volume-title":"Formal Description Techniques VII","author":"Gerard","year":"1995","unstructured":"Gerard J. Holzmann and Doron Peled. An improvement in formal verification . In Formal Description Techniques VII , pages 197 -- 211 . Springer , 1995 . Gerard J. Holzmann and Doron Peled. An improvement in formal verification. In Formal Description Techniques VII, pages 197--211. Springer, 1995."},{"key":"e_1_3_2_1_20_1","first-page":"323","volume-title":"Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Ileri Atalay Mert","year":"2018","unstructured":"Atalay Mert Ileri , Tej Chajed , Adam Chlipala , M. Frans Kaashoek , and Nickolai Zeldovich . Proving confidentiality in a file system using DiskSec . In Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI) , pages 323 -- 338 , Carlsbad, CA , October 2018 . Atalay Mert Ileri, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. Proving confidentiality in a file system using DiskSec. In Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 323--338, Carlsbad, CA, October 2018."},{"volume-title":"Btrfs bug entries","year":"2021","key":"e_1_3_2_1_21_1","unstructured":"Kernel.org Bugzilla. Btrfs bug entries , 2021 . https:\/\/bugzilla.kernel.org\/buglist.cgi?component=btrfs. Kernel.org Bugzilla. Btrfs bug entries, 2021. https:\/\/bugzilla.kernel.org\/buglist.cgi?component=btrfs."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359662"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/379240.379263"},{"key":"e_1_3_2_1_24_1","volume-title":"Proceedings of the USENIX Conference on File and Storage Technologies (FAST)","author":"Lu Lanyue","year":"2013","unstructured":"Lanyue Lu , Andrea C. Arpaci-Dusseau , Remzi H. Arpaci-Dusseau , and Shan Lu . A study of Linux file system evolution . In Proceedings of the USENIX Conference on File and Storage Technologies (FAST) , San Jose, CA , February 2013 . USENIX Association. Lanyue Lu, Andrea C. Arpaci-Dusseau, Remzi H. Arpaci-Dusseau, and Shan Lu. A study of Linux file system evolution. In Proceedings of the USENIX Conference on File and Storage Technologies (FAST), San Jose, CA, February 2013. USENIX Association."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132763"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815422"},{"key":"e_1_3_2_1_27_1","volume-title":"Linux test project (LTP)","author":"Modak Subrata","year":"2009","unstructured":"Subrata Modak . Linux test project (LTP) , 2009 . http:\/\/ltp.sourceforge.net\/. Subrata Modak. Linux test project (LTP), 2009. http:\/\/ltp.sourceforge.net\/."},{"key":"e_1_3_2_1_28_1","first-page":"33","volume-title":"Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Mohan Jayashree","year":"2018","unstructured":"Jayashree Mohan , Ashlie Martinez , Soujanya Ponnapalli , Pandian Raju , and Vijay Chidambaram . Finding crash-consistency bugs with bounded black-box crash testing . In Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI) , pages 33 -- 50 , Carlsbad, CA , October 2018 . Jayashree Mohan, Ashlie Martinez, Soujanya Ponnapalli, Pandian Raju, and Vijay Chidambaram. Finding crash-consistency bugs with bounded black-box crash testing. In Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 33--50, Carlsbad, CA, October 2018."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133373.1133418"},{"key":"e_1_3_2_1_30_1","first-page":"155","volume-title":"Proceedings of the 1st Symposium on Networked Systems Design and Implementation (NSDI)","author":"Musuvathi Madanlal","year":"2004","unstructured":"Madanlal Musuvathi and Dawson R. Engler . Model checking large network protocol implementations . In Proceedings of the 1st Symposium on Networked Systems Design and Implementation (NSDI) , pages 155 -- 168 , San Francisco, CA , March 2004 . Madanlal Musuvathi and Dawson R. Engler. Model checking large network protocol implementations. In Proceedings of the 1st Symposium on Networked Systems Design and Implementation (NSDI), pages 155--168, San Francisco, CA, March 2004."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1060289.1060297"},{"key":"e_1_3_2_1_32_1","unstructured":"NFS-Ganesha 2016. http:\/\/nfs-ganesha.github.io\/.  NFS-Ganesha 2016. http:\/\/nfs-ganesha.github.io\/."},{"key":"e_1_3_2_1_33_1","first-page":"433","volume-title":"Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Pillai Thanumalayan Sankaranarayana","year":"2014","unstructured":"Thanumalayan Sankaranarayana Pillai , Vijay Chidambaram , Ramnatthan Alagappan , Samer Al-Kiswany , Andrea C Arpaci-Dusseau , and Remzi H Arpaci-Dusseau . All file systems are not created equal: On the complexity of crafting crash-consistent applications . In Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI) , pages 433 -- 448 , Broomfield, CO , October 2014 . Thanumalayan Sankaranarayana Pillai, Vijay Chidambaram, Ramnatthan Alagappan, Samer Al-Kiswany, Andrea C Arpaci-Dusseau, and Remzi H Arpaci-Dusseau. All file systems are not created equal: On the complexity of crafting crash-consistent applications. In Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 433--448, Broomfield, CO, October 2014."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095810.1095830"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815411"},{"key":"e_1_3_2_1_36_1","volume-title":"BTRFS: The Linux B-tree filesystem. ACM Transactions on Storage (TOS), 9(3):1--32","author":"Rodeh Ohad","year":"2013","unstructured":"Ohad Rodeh , Josef Bacik , and Chris Mason . BTRFS: The Linux B-tree filesystem. ACM Transactions on Storage (TOS), 9(3):1--32 , 2013 . Ohad Rodeh, Josef Bacik, and Chris Mason. BTRFS: The Linux B-tree filesystem. ACM Transactions on Storage (TOS), 9(3):1--32, 2013."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542506"},{"key":"e_1_3_2_1_38_1","first-page":"167","volume-title":"26th USENIX Security Symposium (USENIX Security)","author":"Schumilo Sergej","year":"2017","unstructured":"Sergej Schumilo , Cornelius Aschermann , Robert Gawlik , Sebastian Schinzel , and Thorsten Holz . kAFL : Hardware-assisted feedback fuzzing for OS kernels . In 26th USENIX Security Symposium (USENIX Security) , pages 167 -- 182 , Vancouver, BC, Canada , August 2017 . Sergej Schumilo, Cornelius Aschermann, Robert Gawlik, Sebastian Schinzel, and Thorsten Holz. kAFL: Hardware-assisted feedback fuzzing for OS kernels. In 26th USENIX Security Symposium (USENIX Security), pages 167--182, Vancouver, BC, Canada, August 2017."},{"key":"e_1_3_2_1_39_1","volume-title":"xfstests","author":"SGI","year":"2016","unstructured":"SGI XFS. xfstests , 2016 . http:\/\/xfs.org\/index.php\/Getting_the_latest_source_code. SGI XFS. xfstests, 2016. http:\/\/xfs.org\/index.php\/Getting_the_latest_source_code."},{"key":"e_1_3_2_1_40_1","first-page":"1","volume-title":"Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Sigurbjarnarson Helgi","year":"2016","unstructured":"Helgi Sigurbjarnarson , James Bornholt , Emina Torlak , and Xi 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 , November 2016 . Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi 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, November 2016."},{"key":"e_1_3_2_1_41_1","unstructured":"Spin Project. Static analysis tools for C code. www.spinroot.com\/static\/.  Spin Project. Static analysis tools for C code. www.spinroot.com\/static\/."},{"key":"e_1_3_2_1_42_1","unstructured":"Miklos Szeredi. Filesystem in Userspace. http:\/\/fuse.sourceforge.net February 2005.  Miklos Szeredi. Filesystem in Userspace. http:\/\/fuse.sourceforge.net February 2005."},{"key":"e_1_3_2_1_43_1","volume-title":"General MTD documentation","author":"Woodhouse David","year":"2009","unstructured":"David Woodhouse , Joern Engel , Jarkko Lavinen , and Artem Bityutskiy . General MTD documentation , 2009 . David Woodhouse, Joern Engel, Jarkko Lavinen, and Artem Bityutskiy. General MTD documentation, 2009."},{"key":"e_1_3_2_1_44_1","unstructured":"David Woodhouse Joern Engel Jarkko Lavinen and Artem Bityutskiy. JFFS2 2009.  David Woodhouse Joern Engel Jarkko Lavinen and Artem Bityutskiy. JFFS2 2009."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134046"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00035"},{"key":"e_1_3_2_1_47_1","first-page":"131","volume-title":"Proceedings of the 7th symposium on Operating systems design and implementation (OSDI)","author":"Yang Junfeng","year":"2006","unstructured":"Junfeng Yang , Can Sar , and Dawson Engler . 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 , November 2006 . Junfeng Yang, Can Sar, and Dawson Engler. 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, November 2006."},{"key":"e_1_3_2_1_48_1","first-page":"273","volume-title":"Proceedings of the 6th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Yang Junfeng","year":"2004","unstructured":"Junfeng Yang , Paul Twohey , Dawson Engler , and Madanlal 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 -- 288 , San Francisco, CA , December 2004 . Junfeng Yang, Paul Twohey, Dawson Engler, and Madanlal 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--288, San Francisco, CA, December 2004."},{"key":"e_1_3_2_1_49_1","volume-title":"On incremental file system development. ACM Transactions on Storage (TOS), 2(2):161--196","author":"Zadok Erez","year":"2006","unstructured":"Erez Zadok , Rakesh Iyer , Nikolai Joukov , Gopalan Sivathanu , and Charles P. Wright . On incremental file system development. ACM Transactions on Storage (TOS), 2(2):161--196 , 2006 . Erez Zadok, Rakesh Iyer, Nikolai Joukov, Gopalan Sivathanu, and Charles P. Wright. On incremental file system development. ACM Transactions on Storage (TOS), 2(2):161--196, 2006."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359644"}],"event":{"name":"HotStorage '21: 13th ACM Workshop on Hot Topics in Storage and File Systems","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX Assoc USENIX Assoc"],"location":"Virtual USA","acronym":"HotStorage '21"},"container-title":["Proceedings of the 13th ACM Workshop on Hot Topics in Storage and File Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3465332.3470878","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3465332.3470878","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3465332.3470878","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:17:11Z","timestamp":1750191431000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3465332.3470878"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,27]]},"references-count":50,"alternative-id":["10.1145\/3465332.3470878","10.1145\/3465332"],"URL":"https:\/\/doi.org\/10.1145\/3465332.3470878","relation":{},"subject":[],"published":{"date-parts":[[2021,7,27]]},"assertion":[{"value":"2021-07-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}