{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,25]],"date-time":"2026-01-25T08:29:04Z","timestamp":1769329744321,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":36,"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":"EPSRC","award":["EP\/K022741\/1, EP\/K008528\/1"],"award-info":[{"award-number":["EP\/K022741\/1, EP\/K008528\/1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,10,4]]},"DOI":"10.1145\/2815400.2815411","type":"proceedings-article","created":{"date-parts":[[2015,10,1]],"date-time":"2015-10-01T12:01:58Z","timestamp":1443700918000},"page":"38-53","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":43,"title":["SibylFS"],"prefix":"10.1145","author":[{"given":"Tom","family":"Ridge","sequence":"first","affiliation":[{"name":"University of Leicester"}]},{"given":"David","family":"Sheets","sequence":"additional","affiliation":[{"name":"University of Cambridge"}]},{"given":"Thomas","family":"Tuerk","sequence":"additional","affiliation":[{"name":"FireEye"}]},{"given":"Andrea","family":"Giugliano","sequence":"additional","affiliation":[{"name":"University of Leicester"}]},{"given":"Anil","family":"Madhavapeddy","sequence":"additional","affiliation":[{"name":"University of Cambridge"}]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge"}]}],"member":"320","published-online":{"date-parts":[[2015,10,4]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"15th Workshop on Hot Topics in Operating Systems (HotOS XV)","author":"Alagappan R.","year":"2015","unstructured":"Alagappan , R. , Chidambaram , V. , Pillai , T. S. , Arpaci-Dusseau , A. C. , and Arpaci-Dusseau , R. H . Beyond storage APIs: Provable semantics for storage stacks . In 15th Workshop on Hot Topics in Operating Systems (HotOS XV) ( Kartause Ittingen, Switzerland , May 2015 ), USENIX Association. Alagappan, R., Chidambaram, V., Pillai, T. S., Arpaci-Dusseau, A. C., and Arpaci-Dusseau, R. H. Beyond storage APIs: Provable semantics for storage stacks. In 15th Workshop on Hot Topics in Operating Systems (HotOS XV) (Kartause Ittingen, Switzerland, May 2015), USENIX Association."},{"key":"e_1_3_2_2_2_1","first-page":"7","volume-title":"Proceedings of the 2009 Conference on USENIX Annual Technical Conference (Berkeley, CA, USA, 2009), USENIX'09, USENIX Association","author":"Bairavasundaram L. N.","unstructured":"Bairavasundaram , L. N. , Sundararaman , S. , Arpaci-Dusseau , A. C. , and Arpaci-Dusseau , R. H . Tolerating file-system mistakes with EnvyFS . In Proceedings of the 2009 Conference on USENIX Annual Technical Conference (Berkeley, CA, USA, 2009), USENIX'09, USENIX Association , pp. 7 -- 7 . Bairavasundaram, L. N., Sundararaman, S., Arpaci-Dusseau, A. C., and Arpaci-Dusseau, R. H. Tolerating file-system mistakes with EnvyFS. In Proceedings of the 2009 Conference on USENIX Annual Technical Conference (Berkeley, CA, USA, 2009), USENIX'09, USENIX Association, pp. 7--7."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1080091.1080123"},{"key":"e_1_3_2_2_4_1","volume-title":"Proceedings of the 15th Workshop on Hot Topics in Operating Systems (HotOS XV)","author":"Chen H.","year":"2015","unstructured":"Chen , H. , Ziegler , D. , Chlipala , A. , Kaashoek , M. F. , Kohler , E. , and Zeldovich , N . Specifying crash safety for storage systems . In Proceedings of the 15th Workshop on Hot Topics in Operating Systems (HotOS XV) ( Kartause Ittingen, Switzerland , May 2015 ). Chen, H., Ziegler, D., Chlipala, A., Kaashoek, M. F., Kohler, E., and Zeldovich, N. Specifying crash safety for storage systems. In Proceedings of the 15th Workshop on Hot Topics in Operating Systems (HotOS XV) (Kartause Ittingen, Switzerland, May 2015)."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522726"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522712"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10452-7_10"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88194-0_5"},{"key":"e_1_3_2_2_9_1","first-page":"242","volume-title":"Experiments VSTTE 2013","author":"Ernst G.","year":"2014","unstructured":"Ernst , G. , Schellhorn , G. , Haneberg , D. , Pf\u00e4hler , J. , and Reif , W . Verification of a virtual filesystem switch. In Verified Software: Theories, Tools , Experiments VSTTE 2013 . Springer , 2014 , pp. 242 -- 261 . Ernst, G., Schellhorn, G., Haneberg, D., Pf\u00e4hler, J., and Reif, W. Verification of a virtual filesystem switch. In Verified Software: Theories, Tools, Experiments VSTTE 2013. Springer, 2014, pp. 242--261."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10452-7_11"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2007.36"},{"key":"e_1_3_2_2_12_1","first-page":"7","volume-title":"Proceedings of the 10th USENIX Conference on File and Storage Technologies (Berkeley, CA, USA, 2012), FAST'12, USENIX Association","author":"Fryer D.","unstructured":"Fryer , D. , Sun , K. , Mahmood , R. , Cheng , T. , Benjamin , S. , Goel , A. , and Brown , A. D . Recon: Verifying file system consistency at runtime . In Proceedings of the 10th USENIX Conference on File and Storage Technologies (Berkeley, CA, USA, 2012), FAST'12, USENIX Association , pp. 7 -- 7 . Fryer, D., Sun, K., Mahmood, R., Cheng, T., Benjamin, S., Goel, A., and Brown, A. D. Recon: Verifying file system consistency at runtime. In Proceedings of the 10th USENIX Conference on File and Storage Technologies (Berkeley, CA, USA, 2012), FAST'12, USENIX Association, pp. 7--7."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_10"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.68"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043564"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0171-2"},{"key":"e_1_3_2_2_17_1","volume-title":"13th USENIX Conference on File and Storage Technologies (FAST 15)","author":"Jannen W.","year":"2015","unstructured":"Jannen , W. , Yuan , J. , Zhan , Y. , Akshintala , A. , Esmet , J. , Jiao , Y. , Mittal , A. , Pandey , P. , Reddy , P. , Walsh , L. , Bender , M. , Farach-Colton , M. , Johnson , R. , Kuszmaul , B. C. , and Porter , D. E . BetrFS: A right-optimized write-optimized file system . In 13th USENIX Conference on File and Storage Technologies (FAST 15) (Santa Clara, CA , Feb. 2015 ), USENIX Association, pp. 301--315. Jannen, W., Yuan, J., Zhan, Y., Akshintala, A., Esmet, J., Jiao, Y., Mittal, A., Pandey, P., Reddy, P., Walsh, L., Bender, M., Farach-Colton, M., Johnson, R., Kuszmaul, B. C., and Porter, D. E. BetrFS: A right-optimized write-optimized file system. In 13th USENIX Conference on File and Storage Technologies (FAST 15) (Santa Clara, CA, Feb. 2015), USENIX Association, pp. 301--315."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87603-8_23"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2626401.2626414"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_2_21_1","unstructured":"Linux Foundation. Linux Standard Base (LSB). http:\/\/www.linuxfoundation.org\/collaborate\/workgroups\/lsb.  Linux Foundation. Linux Standard Base (LSB). http:\/\/www.linuxfoundation.org\/collaborate\/workgroups\/lsb."},{"key":"e_1_3_2_2_22_1","first-page":"03","article-title":"Linux Test Project test-suite. http:\/\/linux-test-project.github.io\/","author":"Linux Test Project","year":"2015","unstructured":"Linux Test Project . Linux Test Project test-suite. http:\/\/linux-test-project.github.io\/ . Accessed 2015 . 03 .26. Linux Test Project. Linux Test Project test-suite. http:\/\/linux-test-project.github.io\/. Accessed 2015.03.26.","journal-title":"Accessed"},{"key":"e_1_3_2_2_23_1","first-page":"31","volume-title":"Presented as part of the 11th USENIX Conference on File and Storage Technologies (FAST 13) (San Jose","author":"Lu L.","year":"2013","unstructured":"Lu , L. , Arpaci-Dusseau , A. C. , Arpaci-Dusseau , R. H. , and Lu , S . A study of Linux file system evolution . In Presented as part of the 11th USENIX Conference on File and Storage Technologies (FAST 13) (San Jose , CA, 2013 ), USENIX , pp. 31 -- 44 . Lu, L., Arpaci-Dusseau, A. C., Arpaci-Dusseau, R. H., and Lu, S. A study of Linux file system evolution. In Presented as part of the 11th USENIX Conference on File and Storage Technologies (FAST 13) (San Jose, CA, 2013), USENIX, pp. 31--44."},{"key":"e_1_3_2_2_24_1","first-page":"75","volume-title":"Proceedings of the 12th USENIX Conference on File and Storage Technologies (FAST 14)","author":"Lu Y.","year":"2014","unstructured":"Lu , Y. , Shu , J. , and Wang , W . ReconFS: A reconstructable file system on flash storage . In Proceedings of the 12th USENIX Conference on File and Storage Technologies (FAST 14) (Santa Clara, CA , 2014 ), USENIX, pp. 75 -- 88 . Lu, Y., Shu, J., and Wang, W. ReconFS: A reconstructable file system on flash storage. In Proceedings of the 12th USENIX Conference on File and Storage Technologies (FAST 14) (Santa Clara, CA, 2014), USENIX, pp. 75--88."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522721"},{"key":"e_1_3_2_2_26_1","first-page":"1","article-title":"Differential testing for software","volume":"10","author":"McKeeman W. M","year":"1998","unstructured":"McKeeman , W. M . Differential testing for software . Digital Technical Journal 10 , 1 ( 1998 ), 100--107. McKeeman, W. M. Differential testing for software. Digital Technical Journal 10, 1 (1998), 100--107.","journal-title":"Digital Technical Journal"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010215"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628143"},{"key":"e_1_3_2_2_29_1","volume-title":"Crash-safe refinement for a verified flash file system. Tech. rep","author":"Pf\u00e4hler J.","year":"2014","unstructured":"Pf\u00e4hler , J. , Ernst , G. , Schellhorn , G. , Haneberg , D. , and Reif , W . Crash-safe refinement for a verified flash file system. Tech. rep ., University of Augsburg , 2014 . Pf\u00e4hler, J., Ernst, G., Schellhorn, G., Haneberg, D., and Reif, W. Crash-safe refinement for a verified flash file system. Tech. rep., University of Augsburg, 2014."},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_21"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_2"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_13"},{"key":"e_1_3_2_2_33_1","volume-title":"2008 Edition. IEEE","author":"The IEEE and The Open Group","year":"2008","unstructured":"The IEEE and The Open Group . The Open Group Base Specifications Issue 7 -- IEEE Std 1003.1 , 2008 Edition. IEEE , New York, NY, USA , 2008 . The IEEE and The Open Group. The Open Group Base Specifications Issue 7 -- IEEE Std 1003.1, 2008 Edition. IEEE, New York, NY, USA, 2008."},{"key":"e_1_3_2_2_34_1","first-page":"03","article-title":"POSIX Conformance Test Suite. http:\/\/www.opengroup.org\/testing\/downloads.html","author":"The Open Group","year":"2015","unstructured":"The Open Group . POSIX Conformance Test Suite. http:\/\/www.opengroup.org\/testing\/downloads.html . Accessed 2015 . 03 .26. The Open Group. POSIX Conformance Test Suite. http:\/\/www.opengroup.org\/testing\/downloads.html. Accessed 2015.03.26.","journal-title":"Accessed"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1189256.1189259"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993532"}],"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.2815411","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2815400.2815411","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:43:13Z","timestamp":1750225393000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2815400.2815411"}},"subtitle":["formal specification and oracle-based testing for POSIX and real-world file systems"],"short-title":[],"issued":{"date-parts":[[2015,10,4]]},"references-count":36,"alternative-id":["10.1145\/2815400.2815411","10.1145\/2815400"],"URL":"https:\/\/doi.org\/10.1145\/2815400.2815411","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"}}]}}