{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T19:50:26Z","timestamp":1730317826490,"version":"3.28.0"},"publisher-location":"New York, NY, USA","reference-count":50,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,3,25]],"date-time":"2016-03-25T00:00:00Z","timestamp":1458864000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,3,25]]},"DOI":"10.1145\/2872362.2872404","type":"proceedings-article","created":{"date-parts":[[2016,3,28]],"date-time":"2016-03-28T13:24:30Z","timestamp":1459171470000},"page":"175-188","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":42,"title":["Cogent"],"prefix":"10.1145","author":[{"given":"Sidney","family":"Amani","sequence":"first","affiliation":[{"name":"Data61 and UNSW, Sydney, Australia"}]},{"given":"Alex","family":"Hixon","sequence":"additional","affiliation":[{"name":"Data61 and UNSW, Sydney, Australia"}]},{"given":"Zilin","family":"Chen","sequence":"additional","affiliation":[{"name":"Data61 and UNSW, Sydney, Australia"}]},{"given":"Christine","family":"Rizkallah","sequence":"additional","affiliation":[{"name":"Data61 and UNSW, Sydney, Australia"}]},{"given":"Peter","family":"Chubb","sequence":"additional","affiliation":[{"name":"Data61 and UNSW, Sydney, Australia"}]},{"given":"Liam","family":"O'Connor","sequence":"additional","affiliation":[{"name":"Data61 and UNSW, Sydney, Australia"}]},{"given":"Joel","family":"Beeren","sequence":"additional","affiliation":[{"name":"Data61 and UNSW, Sydney, Australia"}]},{"given":"Yutaka","family":"Nagashima","sequence":"additional","affiliation":[{"name":"Data61 and UNSW, Sydney, Australia"}]},{"given":"Japheth","family":"Lim","sequence":"additional","affiliation":[{"name":"Data61 and UNSW, Sydney, Australia"}]},{"given":"Thomas","family":"Sewell","sequence":"additional","affiliation":[{"name":"Data61 and UNSW, Sydney, Australia"}]},{"given":"Joseph","family":"Tuong","sequence":"additional","affiliation":[{"name":"Data61 and UNSW, Sydney, Australia"}]},{"given":"Gabriele","family":"Keller","sequence":"additional","affiliation":[{"name":"Data61 and UNSW, Sydney, Australia"}]},{"given":"Toby","family":"Murray","sequence":"additional","affiliation":[{"name":"Data61 and UNSW, Sydney, Australia"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[{"name":"Data61 and UNSW, Sydney, Australia"}]},{"given":"Gernot","family":"Heiser","sequence":"additional","affiliation":[{"name":"Data61 and UNSW, Sydney, Australia"}]}],"member":"320","published-online":{"date-parts":[[2016,3,25]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Numbers 2--4","author":"Alkassar E.","year":"2009","unstructured":"Alkassar , E. , Hillebrand , M. , Leinenbach , D. , Schirmer , N. , Starostin , A. , and Tsyban , A . Balancing the load -- leveraging a semantics stack for systems verification. Journal of Automated Reasoning: Special Issue on Operating System Verification 42 , Numbers 2--4 ( 2009 ), 389--454. Alkassar, E., Hillebrand, M., Leinenbach, D., Schirmer, N., Starostin, A., and Tsyban, A. Balancing the load -- leveraging a semantics stack for systems verification. Journal of Automated Reasoning: Special Issue on Operating System Verification 42, Numbers 2--4 (2009), 389--454."},{"key":"e_1_3_2_1_2_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/978-3-642-15057-9_5","volume-title":"Proceedings of Verified Software: Theories, Tools and Experiments 2010 (Edinburgh","author":"Alkassar E.","year":"2010","unstructured":"Alkassar , E. , Paul , W. , Starostin , A. , and Tsyban , A . Pervasive verification of an OS microkernel: Inline assembly, memory consumption, concurrent devices . In Proceedings of Verified Software: Theories, Tools and Experiments 2010 (Edinburgh , UK , Aug. 2010 ), vol. 6217 of Lecture Notes in Computer Science , pp. 71 -- 85 . Alkassar, E., Paul, W., Starostin, A., and Tsyban, A. Pervasive verification of an OS microkernel: Inline assembly, memory consumption, concurrent devices. In Proceedings of Verified Software: Theories, Tools and Experiments 2010 (Edinburgh, UK, Aug. 2010), vol. 6217 of Lecture Notes in Computer Science, pp. 71--85."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.196.1"},{"key":"e_1_3_2_1_4_1","first-page":"129","volume-title":"J. Formally Proved Anti-tearing Properties of Embedded C Code. In Proceedings of Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation","author":"Andronick","year":"2006","unstructured":"Andronick , J. Formally Proved Anti-tearing Properties of Embedded C Code. In Proceedings of Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation ( Paphos, Cyprus , Nov. 2006 ), pp. 129 -- 136 . Invited Speaker. Andronick, J. Formally Proved Anti-tearing Properties of Embedded C Code. In Proceedings of Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (Paphos, Cyprus, Nov. 2006), pp. 129--136. Invited Speaker."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30482-1_32"},{"key":"e_1_3_2_1_6_1","series-title":"An EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science","author":"Bertot Y.","year":"2004","unstructured":"Bertot , Y. , and Cast\u00e9ran , P . Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science . An EATCS Series . 2004 . Bertot, Y., and Cast\u00e9ran, P. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. 2004."},{"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","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88194-0_5"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522720"},{"key":"e_1_3_2_1_11_1","series-title":"Lecture Notes in Computer Science","first-page":"242","volume-title":"Proceedings of Verified Software: Theories, Tools and Experiments 2013 (Menlo Park","author":"Ernst G.","year":"2013","unstructured":"Ernst , G. , Schellhorn , G. , Haneberg , D. , Pfahler , J. , and Reif , W . Verification of a virtual filesystem switch . In Proceedings of Verified Software: Theories, Tools and Experiments 2013 (Menlo Park , CA , USA , May 2013 ), vol. 8164 of Lecture Notes in Computer Science , pp. 242 -- 261 . Ernst, G., Schellhorn, G., Haneberg, D., Pfahler, J., and Reif, W. Verification of a virtual filesystem switch. In Proceedings of Verified Software: Theories, Tools and Experiments 2013 (Menlo Park, CA, USA, May 2013), vol. 8164 of Lecture Notes in Computer Science, pp. 242--261."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103799.2103803"},{"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","first-page":"207","volume-title":"Proceedings of the 6th USENIX Conference on File and Storage Technologies (Feb.","author":"Gunawi H. S.","year":"2008","unstructured":"Gunawi , H. S. , Rubio-Gonz\u00e1lez , C. , Arpaci-Dusseau , A. C. , Arpaci-Dussea , R. H. , and Liblit , B . EIO: error handling is occasionally correct . In Proceedings of the 6th USENIX Conference on File and Storage Technologies (Feb. 2008 ), pp. 207 -- 222 . Gunawi, H. S., Rubio-Gonz\u00e1lez, C., Arpaci-Dusseau, A. C., Arpaci-Dussea, R. H., and Liblit, B. EIO: error handling is occasionally correct. In Proceedings of the 6th USENIX Conference on File and Storage Technologies (Feb. 2008), pp. 207--222."},{"key":"e_1_3_2_1_15_1","first-page":"165","volume-title":"USENIX Symposium on Operating Systems Design and Implementation","author":"Hawblitzel C.","year":"2014","unstructured":"Hawblitzel , C. , Howell , J. , Lorch , J. R. , Narayan , A. , Parno , B. , Zhang , D. , and Zill , B . Ironclad apps: End-to-end security via automated full-system verification . In USENIX Symposium on Operating Systems Design and Implementation ( Broomfield, CO, US , Oct. 2014 ), pp. 165 -- 181 . Hawblitzel, C., Howell, J., Lorch, J. R., Narayan, A., Parno, B., Zhang, D., and Zill, B. Ironclad apps: End-to-end security via automated full-system verification. In USENIX Symposium on Operating Systems Design and Implementation (Broomfield, CO, US, Oct. 2014), pp. 165--181."},{"key":"e_1_3_2_1_16_1","volume-title":"Apr.","author":"The Heartbleed","year":"2014","unstructured":"The Heartbleed bug. http:\/\/heartbleed.com, https:\/\/www.openssl.org\/news\/secadv_20140407.txt , Apr. 2014 . Accessed March 2015. The Heartbleed bug. http:\/\/heartbleed.com, https:\/\/www.openssl.org\/news\/secadv_20140407.txt, Apr. 2014. Accessed March 2015."},{"key":"e_1_3_2_1_17_1","volume-title":"MINIX 3: A highly reliable, self-repairing operating system. ACM Operating Systems Review 40, 3 (July","author":"Herder J. N.","year":"2006","unstructured":"Herder , J. N. , Bos , H. , Gras , B. , Homburg , P. , and Tanenbaum , A. S . MINIX 3: A highly reliable, self-repairing operating system. ACM Operating Systems Review 40, 3 (July 2006 ), 80--89. Herder, J. N., Bos, H., Gras, B., Homburg, P., and Tanenbaum, A. S. MINIX 3: A highly reliable, self-repairing operating system. ACM Operating Systems Review 40, 3 (July 2006), 80--89."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.12.018"},{"key":"e_1_3_2_1_19_1","volume-title":"A brief introduction to the design of UBIFS, 03","author":"Hunter A.","year":"2008","unstructured":"Hunter , A. A brief introduction to the design of UBIFS, 03 2008 . Hunter, A. A brief introduction to the design of UBIFS, 03 2008."},{"key":"e_1_3_2_1_20_1","unstructured":"IOzone filesystem benchmark. http:\/\/www.iozone.org\/. IOzone filesystem benchmark. http:\/\/www.iozone.org\/."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0022-3"},{"key":"e_1_3_2_1_23_1","first-page":"1","volume-title":"USA","author":"Keller G.","year":"2013","unstructured":"Keller , G. , Murray , T. , Amani , S. , O'Connor-Davis , L. , Chen , Z. , Ryzhyk , L. , Klein , G. , and Heiser , G . File systems deserve verification too! In Workshop on Programming Languages and Operating Systems (PLOS) (Farmington, Pennsylvania , USA , Nov. 2013 ), pp. 1 -- 7 . Keller, G., Murray, T., Amani, S., O'Connor-Davis, L., Chen, Z., Ryzhyk, L., Klein, G., and Heiser, G. File systems deserve verification too! In Workshop on Programming Languages and Operating Systems (PLOS) (Farmington, Pennsylvania, USA, Nov. 2013), pp. 1--7."},{"key":"e_1_3_2_1_24_1","volume-title":"Operating system verification -- an overview. S\\=adhan\\=a 34, 1 (Feb","author":"Klein G.","year":"2009","unstructured":"Klein , G. Operating system verification -- an overview. S\\=adhan\\=a 34, 1 (Feb . 2009 ), 27--69. Klein, G. Operating system verification -- an overview. S\\=adhan\\=a 34, 1 (Feb. 2009), 27--69."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/168619.168633"},{"key":"e_1_3_2_1_30_1","volume-title":"Dec.","author":"Memory","year":"2014","unstructured":"Memory leak in Android Lollipop's rendering engine. https:\/\/code.google.com\/p\/android\/issues\/detail?id=79729#c177 , Dec. 2014 . Accessed March 2015. Memory leak in Android Lollipop's rendering engine. https:\/\/code.google.com\/p\/android\/issues\/detail?id=79729#c177, Dec. 2014. Accessed March 2015."},{"key":"e_1_3_2_1_31_1","first-page":"449","volume-title":"Proceedings of the 19th International Symposium on Formal Methods (FM) (May","volume":"8442","author":"Maric O.","year":"2014","unstructured":"Maric , O. , and Sprenger , C . Verification of a transactional memory manager under hardware failures and restarts . In Proceedings of the 19th International Symposium on Formal Methods (FM) (May 2014 ), vol. 8442 of Lecture Notes in Computer Science , pp. 449 -- 464 . Maric, O., and Sprenger, C. Verification of a transactional memory manager under hardware failures and restarts. In Proceedings of the 19th International Symposium on Formal Methods (FM) (May 2014), vol. 8442 of Lecture Notes in Computer Science, pp. 449--464."},{"key":"e_1_3_2_1_32_1","first-page":"11","volume-title":"International Conference on Software Engineering","author":"Matichuk D.","year":"2015","unstructured":"Matichuk , D. , Murray , T. , Andronick , J. , Jeffery , R. , Klein , G. , and Staples , M . Empirical study towards a leading indicator for cost of formal software verification . In International Conference on Software Engineering ( Firenze, Italy , Feb. 2015 ), p. 11 . Matichuk, D., Murray, T., Andronick, J., Jeffery, R., Klein, G., and Staples, M. Empirical study towards a leading indicator for cost of formal software verification. In International Conference on Software Engineering (Firenze, Italy, Feb. 2015), p. 11."},{"key":"e_1_3_2_1_33_1","first-page":"2","article-title":"Specification of the UNIX filing system","volume":"10","author":"Morgan C.","year":"1984","unstructured":"Morgan , C. , and Sufrin , B . Specification of the UNIX filing system . IEEE Transactions on Software Engineering 10 , 2 ( 1984 ), 128--142. Morgan, C., and Sufrin, B. Specification of the UNIX filing system. IEEE Transactions on Software Engineering 10, 2 (1984), 128--142.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"e_1_3_2_1_34_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL -- A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"Nipkow , T. , Paulson , L. , and Wenzel , M . Isabelle\/HOL -- A Proof Assistant for Higher-Order Logic , vol. 2283 of Lecture Notes in Computer Science . 2002 . Nipkow, T., Paulson, L., and Wenzel, M. Isabelle\/HOL -- A Proof Assistant for Higher-Order Logic, vol. 2283 of Lecture Notes in Computer Science. 2002."},{"key":"e_1_3_2_1_35_1","volume-title":"Retrieved","author":"POSIX","year":"2016","unstructured":"POSIX filesystem test project. http:\/\/sourceforge.net\/p\/ntfs-3g\/pjd-fstest\/ci\/master\/tree\/ . Retrieved Jan. , 2016 . POSIX filesystem test project. http:\/\/sourceforge.net\/p\/ntfs-3g\/pjd-fstest\/ci\/master\/tree\/. Retrieved Jan., 2016."},{"key":"e_1_3_2_1_36_1","volume-title":"textscCOGENT: Certified compilation for a functional systems language. CoRR abs\/1601.05520","author":"O'Connor L.","year":"2016","unstructured":"O'Connor , L. , Rizkallah , C. , Chen , Z. , Amani , S. , Lim , J. , Nagashima , Y. , Sewell , T. , Hixon , A. , Keller , G. , Murray , T. , and Klein , G . textscCOGENT: Certified compilation for a functional systems language. CoRR abs\/1601.05520 ( 2016 ). O'Connor, L., Rizkallah, C., Chen, Z., Amani, S., Lim, J., Nagashima, Y., Sewell, T., Hixon, A., Keller, G., Murray, T., and Klein, G.textscCOGENT: Certified compilation for a functional systems language. CoRR abs\/1601.05520 (2016)."},{"key":"e_1_3_2_1_37_1","volume-title":"Feb.","author":"Apple's","year":"2014","unstructured":"Apple's SSL\/TLS bug. https:\/\/www.imperialviolet.org\/2014\/02\/22\/applebug.html , Feb. 2014 . Accessed March 2015. Apple's SSL\/TLS bug. https:\/\/www.imperialviolet.org\/2014\/02\/22\/applebug.html, Feb. 2014. Accessed March 2015."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950401"},{"key":"e_1_3_2_1_39_1","series-title":"Applied Logic Series","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1007\/978-94-017-0435-9_1","volume-title":"Automated Deduction -- A Basis for Applications","author":"Reif W.","year":"1998","unstructured":"Reif , W. , Schellhorn , G. , Stenzel , K. , and Balser , M . Structured specifications and interactive proofs with KIV . In Automated Deduction -- A Basis for Applications , vol. 9 of Applied Logic Series . 1998 , pp. 13 -- 39 . Reif, W., Schellhorn, G., Stenzel, K., and Balser, M. Structured specifications and interactive proofs with KIV. In Automated Deduction -- A Basis for Applications, vol. 9 of Applied Logic Series. 1998, pp. 13--39."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001434"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1967677.1967684"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2013.6575307"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_2"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_13"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217951"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2024724.2024733"},{"key":"e_1_3_2_1_49_1","volume-title":"Linear types can change the world! In Programming Concepts and Methods","author":"Wadler P.","year":"1990","unstructured":"Wadler , P. Linear types can change the world! In Programming Concepts and Methods ( 1990 ). Wadler, P. Linear types can change the world! In Programming Concepts and Methods (1990)."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_34"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806610"},{"key":"e_1_3_2_1_52_1","first-page":"131","volume-title":"USENIX Symposium on Operating Systems Design and Implementation (Nov.","author":"Yang J.","year":"2006","unstructured":"Yang , J. , Sar , C. , and Engler , D . EXPLODE: a lightweight, general system for finding serious storage system errors . In USENIX Symposium on Operating Systems Design and Implementation (Nov. 2006 ), pp. 131 -- 146 . Yang, J., Sar, C., and Engler, D. EXPLODE: a lightweight, general system for finding serious storage system errors. In USENIX Symposium on Operating Systems Design and Implementation (Nov. 2006), pp. 131--146."}],"event":{"name":"ASPLOS '16: Architectural Support for Programming Languages and Operating Systems","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGOPS ACM Special Interest Group on Operating Systems","SIGARCH ACM Special Interest Group on Computer Architecture","SIGBED ACM Special Interest Group on Embedded Systems"],"location":"Atlanta Georgia USA","acronym":"ASPLOS '16"},"container-title":["Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2872362.2872404","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T15:05:12Z","timestamp":1693839912000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2872362.2872404"}},"subtitle":["Verifying High-Assurance File System Implementations"],"short-title":[],"issued":{"date-parts":[[2016,3,25]]},"references-count":50,"alternative-id":["10.1145\/2872362.2872404","10.1145\/2872362"],"URL":"https:\/\/doi.org\/10.1145\/2872362.2872404","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2954679.2872404","asserted-by":"object"},{"id-type":"doi","id":"10.1145\/2980024.2872404","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,3,25]]},"assertion":[{"value":"2016-03-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}