{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:11:33Z","timestamp":1760044293239,"version":"3.41.0"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,5,15]],"date-time":"2014-05-15T00:00:00Z","timestamp":1400112000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGOPS Oper. Syst. Rev."],"published-print":{"date-parts":[[2014,5,15]]},"abstract":"<jats:p>File systems are too important, and current ones are too buggy, to remain unverified. Yet the most successful verification methods for functional correctness remain too expensive for current file system implementations-we need verified correctness but at reasonable cost. This paper presents our vision and ongoing work to achieve this goal for a new high-performance flash file system, called BilbyFs. BilbyFs is carefully designed to be highly modular, so it can be verified against a high-level functional specification one component at a time. This modular implementation is captured in a set of domain specific languages from which we produce the design-level specification, as well as its optimised C implementation. Importantly, we also automatically generate the proof linking these two artefacts. The combination of these features dramatically reduces verification effort. Verified file systems are now within reach for the first time.<\/jats:p>","DOI":"10.1145\/2626401.2626414","type":"journal-article","created":{"date-parts":[[2014,5,20]],"date-time":"2014-05-20T13:47:43Z","timestamp":1400593663000},"page":"58-64","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["File systems deserve verification too!"],"prefix":"10.1145","volume":"48","author":[{"given":"Gabriele","family":"Keller","sequence":"first","affiliation":[{"name":"NICTA, Sydney, Australia and University of New South Wales, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Toby","family":"Murray","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia and University of New South Wales, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sidney","family":"Amani","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia and University of New South Wales, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Liam","family":"O'Connor","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia and University of New South Wales, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zilin","family":"Chen","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia and University of New South Wales, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonid","family":"Ryzhyk","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia, University of New South Wales, Australia and University of Toronto, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia and University of New South Wales, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gernot","family":"Heiser","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia and University of New South Wales, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,5,15]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/645435.652647"},{"key":"e_1_2_1_2_1","first-page":"35","volume-title":"Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design","author":"Ball T.","year":"2010","unstructured":"T. Ball , E. Bounimova , R. Kumar , and V. Levin . SLAM2: Static driver verification with under 4% false alarms . In Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design , pages 35 -- 42 , Lugano, Switzerland , 2010 . FMCAD Inc. T. Ball, E. Bounimova, R. Kumar, and V. Levin. SLAM2: Static driver verification with under 4% false alarms. In Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, pages 35--42, Lugano, Switzerland, 2010. FMCAD Inc."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646374"},{"key":"e_1_2_1_4_1","series-title":"CEUR Workshop Proceedings","first-page":"44","volume-title":"Proceedings of the 5th International Verification Workshop","author":"Cock D.","year":"2008","unstructured":"D. Cock . Bitfields and tagged unions in C: Verification through automatic generation . In B. Beckert and G. Klein, editors, Proceedings of the 5th International Verification Workshop , volume 372 of CEUR Workshop Proceedings , pages 44 -- 55 , Sydney , Australia, Aug . 2008 . D. Cock. Bitfields and tagged unions in C: Verification through automatic generation. In B. Beckert and G. Klein, editors, Proceedings of the 5th International Verification Workshop, volume 372 of CEUR Workshop Proceedings, pages 44--55, Sydney, Australia, Aug. 2008."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.09.061"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1938551.1938556"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667053.1667059"},{"key":"e_1_2_1_8_1","unstructured":"D.\n      Greenaway J.\n      Andronick and \n      G.\n      Klein\n  . \n  Bridging the gap: Automatic verified abstraction of C\n  . In L. Beringer and A. Felty editors 3rd International Conference on Interactive Theorem Proving volume \n  7406\n   of \n  Lecture Notes in Computer Science pages \n  99\n  --\n  115 Princeton New Jersey Aug. \n  2012\n  . \n  Springer\n  . ISBN 978- 3-642-32346-1.  D. Greenaway J. Andronick and G. Klein. Bridging the gap: Automatic verified abstraction of C. In L. Beringer and A. Felty editors 3rd International Conference on Interactive Theorem Proving volume 7406 of Lecture Notes in Computer Science pages 99--115 Princeton New Jersey Aug. 2012. Springer. ISBN 978- 3-642-32346-1."},{"key":"e_1_2_1_9_1","first-page":"1","volume-title":"Workshop on Hot Topics in Operating Systems","author":"Jannen W.","year":"2013","unstructured":"W. Jannen , C.-C. Tsai , and D. E. Porter . Virtualize storage, not disks . In Workshop on Hot Topics in Operating Systems , pages 1 -- 7 , Santa Ana Pueblo, NM, USA , May 2013 . W. Jannen, C.-C. Tsai, and D. E. Porter. Virtualize storage, not disks. In Workshop on Hot Topics in Operating Systems, pages 1--7, Santa Ana Pueblo, NM, USA, May 2013."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_12_1","volume-title":"USENIX Conference on File and Storage Technologies","author":"Lu L.","year":"2013","unstructured":"L. Lu , A. C. Arpaci-Dusseau , R. H. Arpaci-Dusseau , and S. Lu . A study of Linux file system evolution . In USENIX Conference on File and Storage Technologies , San Jose, CA, USA , Feb. 2013 . L. Lu, A. C. Arpaci-Dusseau, R. H. Arpaci-Dusseau, and S. Lu. A study of Linux file system evolution. In USENIX Conference on File and Storage Technologies, San Jose, CA, USA, Feb. 2013."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/347059.347563"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950401"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1967677.1967684"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"e_1_2_1_17_1","volume-title":"Linear types can change the world! In Programming Concepts and Methods","author":"Wadler P.","year":"1990","unstructured":"P. Wadler . Linear types can change the world! In Programming Concepts and Methods , 1990 . P. Wadler. Linear types can change the world! In Programming Concepts and Methods, 1990."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1189256.1189259"}],"container-title":["ACM SIGOPS Operating Systems Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2626401.2626414","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2626401.2626414","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:19:42Z","timestamp":1750231182000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2626401.2626414"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,5,15]]},"references-count":18,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,5,15]]}},"alternative-id":["10.1145\/2626401.2626414"],"URL":"https:\/\/doi.org\/10.1145\/2626401.2626414","relation":{},"ISSN":["0163-5980"],"issn-type":[{"type":"print","value":"0163-5980"}],"subject":[],"published":{"date-parts":[[2014,5,15]]},"assertion":[{"value":"2014-05-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}