{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:13:10Z","timestamp":1781892790541,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":18,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,11,3]],"date-time":"2013-11-03T00:00:00Z","timestamp":1383436800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000935","name":"Department of Broadband, Communications and the Digital Economy , Australian Government","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000935","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-12-9-0179"],"award-info":[{"award-number":["FA8750-12-9-0179"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,11,3]]},"DOI":"10.1145\/2525528.2525530","type":"proceedings-article","created":{"date-parts":[[2013,10,17]],"date-time":"2013-10-17T12:23:54Z","timestamp":1382012634000},"page":"1-7","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["File systems deserve verification too!"],"prefix":"10.1145","author":[{"given":"Gabriele","family":"Keller","sequence":"first","affiliation":[{"name":"NICTA, Sydney, Australia and University of New South Wales, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Toby","family":"Murray","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia and University of New South Wales, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sidney","family":"Amani","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia and University of New South Wales, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Liam","family":"O'Connor","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia and University of New South Wales, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zilin","family":"Chen","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia and University of New South Wales, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Leonid","family":"Ryzhyk","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia and University of New South Wales, Australia and University of Toronto, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia and University of New South Wales, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gernot","family":"Heiser","sequence":"additional","affiliation":[{"name":"NICTA, Sydney, Australia and University of New South Wales, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2013,11,3]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/645435.652647"},{"key":"e_1_3_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_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646374"},{"key":"e_1_3_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_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.09.061"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1938551.1938556"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667053.1667059"},{"key":"e_1_3_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_3_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_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_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_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/347059.347563"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950401"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1967677.1967684"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"e_1_3_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_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1189256.1189259"}],"event":{"name":"SOSP '13: ACM SIGOPS 24th Symposium on Operating Systems Principles","location":"Farmington Pennsylvania","acronym":"SOSP '13","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"]},"container-title":["Proceedings of the Seventh Workshop on Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2525528.2525530","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2525528.2525530","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:24Z","timestamp":1750231704000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2525528.2525530"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11,3]]},"references-count":18,"alternative-id":["10.1145\/2525528.2525530","10.1145\/2525528"],"URL":"https:\/\/doi.org\/10.1145\/2525528.2525530","relation":{},"subject":[],"published":{"date-parts":[[2013,11,3]]},"assertion":[{"value":"2013-11-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}