{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T21:00:16Z","timestamp":1730322016265,"version":"3.28.0"},"publisher-location":"New York, NY, USA","reference-count":69,"publisher":"ACM","funder":[{"name":"National Key Research and Development Program of China","award":["#2018YFB1004805"]},{"name":"National Natural Science Foundation of China","award":["#61932021, #61690204, #61802165"]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,6,27]]},"DOI":"10.1145\/3377811.3380350","type":"proceedings-article","created":{"date-parts":[[2020,10,1]],"date-time":"2020-10-01T18:25:38Z","timestamp":1601576738000},"page":"1483-1495","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Testing file system implementations on layered models"],"prefix":"10.1145","author":[{"given":"Dongjie","family":"Chen","sequence":"first","affiliation":[{"name":"Nanjing University, Nanjing, China"}]},{"given":"Yanyan","family":"Jiang","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}]},{"given":"Chang","family":"Xu","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}]},{"given":"Xiaoxing","family":"Ma","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}]},{"given":"Jian","family":"Lu","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}]}],"member":"320","published-online":{"date-parts":[[2020,10]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n.d.]. Bug #317781: Ext4 Data Loss. https:\/\/bugs.launchpad.net\/ubuntu\/+source\/linux\/+bug\/317781?comments=all."},{"key":"e_1_3_2_1_2_1","unstructured":"[n.d.]. Debootstrap - Debian Wiki. https:\/\/wiki.debian.org\/Debootstrap."},{"key":"e_1_3_2_1_3_1","unstructured":"[n.d.]. Kernel: Add Kcov Code Coverage. https:\/\/lwn.net\/Articles\/671640\/."},{"key":"e_1_3_2_1_4_1","unstructured":"[n.d.]. Linux Programmer's Manual UNLINK(2). http:\/\/man7.org\/linux\/man-pages\/man2\/unlink.2.html."},{"key":"e_1_3_2_1_5_1","unstructured":"[n.d.]. Syzkaller. https:\/\/github.com\/google\/syzkaller."},{"key":"e_1_3_2_1_6_1","unstructured":"[n.d.]. (x)fstests Is A Filesystem Testing Suite. https:\/\/github.com\/kdave\/xfstests."},{"key":"e_1_3_2_1_7_1","unstructured":"2015. Btrfs: Add Missing Inode Update When Punching Hole. https:\/\/patchwork.kernel.org\/patch\/5830801\/."},{"key":"e_1_3_2_1_8_1","unstructured":"Alexandr Andoni Dumitru Daniliuc Sarfraz Khurshid and Darko Marinov. 2003. Evaluating the \"Small Scope Hypothesis\". Citeseer."},{"volume-title":"Verifying a File System Implementation","author":"Arkoudas Konstantine","key":"e_1_3_2_1_9_1","unstructured":"Konstantine Arkoudas, Karen Zee, Viktor Kuncak, and Martin Rinard. 2004. Verifying a File System Implementation. In Formal Methods and Software Engineering, Jim Davies, Wolfram Schulte, and Mike Barnett (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 373--390."},{"key":"e_1_3_2_1_10_1","volume-title":"NAUTILUS: Fishing for Deep Bugs with Grammars. In NDSS.","author":"Aschermann Cornelius","year":"2019","unstructured":"Cornelius Aschermann, Tommaso Frassetto, Thorsten Holz, Patrick Jauernig, Ahmad-Reza Sadeghi, and Daniel Teuchert. 2019. NAUTILUS: Fishing for Deep Bugs with Grammars. In NDSS."},{"key":"e_1_3_2_1_11_1","unstructured":"Farbrice Bellard. [n.d.]. Tiny C Compiler. https:\/\/bellard.org\/tcc\/."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1247360.1247401"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.2161"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872406"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-002-0004-8"},{"key":"e_1_3_2_1_16_1","series-title":"Springer LNCS","volume-title":"Model-based Testing of Reactive Systems","author":"Broy Manfred","unstructured":"Manfred Broy, Bengt Jonsson, J-P Katoen, Martin Leucker, and Alexander Pretschner. 2005. Model-based Testing of Reactive Systems. In Volume 3472 of Springer LNCS. Springer."},{"volume-title":"Proceedings of the 36th International Conference on Software Engineering (ICSE '14)","author":"Cai Yan","key":"e_1_3_2_1_17_1","unstructured":"Yan Cai, Shangru Wu, and W. K. Chan. 2014. ConLock: A Constraint-based Approach to Dynamic Checking on Deadlocks in Multithreaded Programs. In Proceedings of the 36th International Conference on Software Engineering (ICSE '14). ACM, New York, NY, USA, 491--502."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236077"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1978.231496"},{"key":"e_1_3_2_1_21_1","unstructured":"Mason Chris. 2007. The Btrfs Filesystem. http:\/\/oss.oracle.com\/projects\/btrfs\/dist\/documentation\/btrfs-ukuug.pdf."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA461189"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Arilo C Dias Neto Rajesh Subramanyan Marlon Vieira and Guilherme H Travassos. 2007. A Survey on Model-based Testing Approaches: A Systematic Review. In Proceedings of the 1st ACM international workshop on Empirical assessment of software engineering languages and technologies: held in conjunction with the 22nd IEEE\/ACM International Conference on Automated Software Engineering (ASE '07). ACM 31--36.","DOI":"10.1145\/1353673.1353681"},{"key":"e_1_3_2_1_24_1","volume-title":"Delay-bounded Scheduling. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '11)","author":"Emmi Michael","year":"2011","unstructured":"Michael Emmi, Shaz Qadeer, and Zvonimir Rakamari\u0107. 2011. Delay-bounded Scheduling. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '11). ACM, New York, NY, USA, 411--422."},{"volume-title":"Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation (OSDI '14)","author":"Fonseca Pedro","key":"e_1_3_2_1_25_1","unstructured":"Pedro Fonseca, Rodrigo Rodrigues, and Bj\u00f6rn B. Brandenburg. 2014. SKI: Exposing Kernel Concurrency Bugs Through Systematic Schedule Exploration. In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation (OSDI '14). USENIX Association, Berkeley, CA, USA, 415--431."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-016-9338-2"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Nikolas Havrikov and Andreas Zeller. 2019. Systematically Covering Input Structure. (2019).","DOI":"10.1109\/ASE.2019.00027"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236083"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3278186.3278193"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.585157"},{"key":"e_1_3_2_1_32_1","first-page":"1","article-title":"Alloy: A Logical Modelling Language","volume":"2651","author":"Jackson Daniel","year":"2003","unstructured":"Daniel Jackson. 2003. Alloy: A Logical Modelling Language. ZB 2651 (2003), 1.","journal-title":"ZB"},{"volume-title":"Proceedings of the 1996 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA '96)","author":"Jackson Daniel","key":"e_1_3_2_1_33_1","unstructured":"Daniel Jackson and Craig A. Damon. 1996. Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector. In Proceedings of the 1996 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA '96). ACM, New York, NY, USA, 239--249."},{"key":"e_1_3_2_1_34_1","unstructured":"Edge Jake. 2014. The Kernel Address Sanitizer. https:\/\/lwn.net\/Articles\/612153\/."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132767"},{"key":"e_1_3_2_1_36_1","unstructured":"Brian W Kernighan and Dennis M Ritchie. 2006. The C programming language."},{"volume-title":"Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '07)","author":"Killian Charles Edwin","key":"e_1_3_2_1_37_1","unstructured":"Charles Edwin Killian, James W. Anderson, Ryan Braud, Ranjit Jhala, and Amin M. Vahdat. 2007. Mace: Language Support for Building Distributed Systems. In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '07). ACM, New York, NY, USA, 179--188."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594334"},{"key":"e_1_3_2_1_39_1","article-title":"A Study of Linux File System","volume":"10","author":"Lu Lanyue","year":"2014","unstructured":"Lanyue Lu, Andrea C. Arpaci-Dusseau, Remzi H. Arpaci-Dusseau, and Shan Lu. 2014. A Study of Linux File System Evolution. Trans. Storage 10, 1, Article 3 (Jan. 2014), 32 pages.","journal-title":"Evolution. Trans. Storage"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1346281.1346323"},{"key":"e_1_3_2_1_41_1","volume-title":"Proceedings of the 9th USENIX Conference on Hot Topics in Storage and File Systems (HotStorage '17)","author":"Martinez Ashlie","year":"2017","unstructured":"Ashlie Martinez and Vijay Chidambaram. 2017. Crashmonkey: A Framework to Systematically Test File-system Crash Consistency. In Proceedings of the 9th USENIX Conference on Hot Topics in Storage and File Systems (HotStorage '17). USENIX Association, Berkeley, CA, USA, 6--6."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/646752.704751"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815422"},{"key":"e_1_3_2_1_44_1","volume-title":"Proceedings of the 27th Symposium on Operating Systems Principles (SOSP '19)","author":"Mo Zou","year":"2019","unstructured":"Zou Mo, Ding Haoran, Du Dong, Fu Ming, Ronghui Gu, and Chen Haibo. 2019. Using Concurrent Relational Logic with Helper for Verifying the AtomFS File System. In Proceedings of the 27th Symposium on Operating Systems Principles (SOSP '19). ACM, New York, NY, USA."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/3291168.3291172"},{"key":"e_1_3_2_1_46_1","unstructured":"Steven Muchnick et al. 1997. Advanced compiler design implementation. Morgan kaufmann."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/2228298.2228334"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/2337223.2337309"},{"key":"e_1_3_2_1_50_1","volume-title":"Filesystem Fuzzing with American Fuzzy Lop. Vault 2016","author":"Nossum Vegard","year":"2016","unstructured":"Vegard Nossum and Quentin Casasnovas. 2016. Filesystem Fuzzing with American Fuzzy Lop. Vault 2016 (2016)."},{"volume-title":"Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation (OSDI '14)","author":"Pillai Thanumalayan Sankaranarayana","key":"e_1_3_2_1_51_1","unstructured":"Thanumalayan Sankaranarayana Pillai, Vijay Chidambaram, Ramnatthan Alagappan, Samer Al-Kiswany, Andrea C. Arpaci-Dusseau, and Remzi H. Arpaci-Dusseau. 2014. All File Systems Are Not Created Equal: On the Complexity of Crafting Crash-consistent Applications. In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation (OSDI '14). USENIX Association, Berkeley, CA, USA, 433--448."},{"key":"e_1_3_2_1_52_1","unstructured":"Hat Red. 2005. libvirt: The virtualization API. https:\/\/libvirt.org\/."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815411"},{"key":"e_1_3_2_1_54_1","article-title":"BTRFS","volume":"9","author":"Rodeh Ohad","year":"2013","unstructured":"Ohad Rodeh, Josef Bacik, and Chris Mason. 2013. BTRFS: The Linux B-Tree Filesystem. Trans. Storage 9, 3, Article 9 (Aug. 2013), 32 pages.","journal-title":"The Linux B-Tree Filesystem. Trans. Storage"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375584"},{"volume-title":"Presented as part of the 2012 USENIX Annual Technical Conference (USENIX ATC '12)","author":"Serebryany Konstantin","key":"e_1_3_2_1_56_1","unstructured":"Konstantin Serebryany, Derek Bruening, Alexander Potapenko, and Dmitriy Vyukov. 2012. AddressSanitizer: A Fast Address Sanity Checker. In Presented as part of the 2012 USENIX Annual Technical Conference (USENIX ATC '12). USENIX, Boston, MA, 309--318."},{"key":"e_1_3_2_1_57_1","volume-title":"Self-securing Storage: Protecting Data in Compromised Systems. In Foundations of Intrusion Tolerant Systems","author":"Strunk J. D.","year":"2003","unstructured":"J. D. Strunk, G. R. Goodson, M. L. Scheinholtz, C. A. N. Soules, and G. R. Ganger. 2003. Self-securing Storage: Protecting Data in Compromised Systems. In Foundations of Intrusion Tolerant Systems, 2003 [Organically Assured and Survivable Information Systems]. 195--209."},{"key":"e_1_3_2_1_58_1","unstructured":"Goswami Sudhanshu. 2005. An introduction to KProbes. https:\/\/lwn.net\/Articles\/132196\/."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.12.014"},{"key":"e_1_3_2_1_60_1","volume-title":"Torx: Automated Model-based Testing. In First European Conference on Model-Driven Software Engineering. 31--43","author":"Tretmans GJ","year":"2003","unstructured":"GJ Tretmans and Hendrik Brinksma. 2003. Torx: Automated Model-based Testing. In First European Conference on Model-Driven Software Engineering. 31--43."},{"volume-title":"Formal methods and testing","author":"Tretmans Jan","key":"e_1_3_2_1_61_1","unstructured":"Jan Tretmans. 2008. Model Based Testing with Labelled Transition Systems. In Formal methods and testing. Springer, 1--38."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.456"},{"volume-title":"Formal methods and testing","author":"Veanes Margus","key":"e_1_3_2_1_63_1","unstructured":"Margus Veanes, Colin Campbell, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, and Lev Nachmanson. 2008. Model-based Testing of Object-oriented Reactive Systems with Spec Explorer. In Formal methods and testing. Springer, 39--76."},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.328991"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00035"},{"key":"e_1_3_2_1_67_1","volume-title":"MODIST: Transparent Model Checking of Unmodified Distributed Systems.","author":"Yang Junfeng","year":"2009","unstructured":"Junfeng Yang, Tisheng Chen, Ming Wu, Zhilei Xu, Xuezheng Liu, Haoxiang Lin, Mao Yang, Fan Long, Lintao Zhang, and Lidong Zhou. 2009. MODIST: Transparent Model Checking of Unmodified Distributed Systems. (2009)."},{"key":"e_1_3_2_1_68_1","volume-title":"Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation -","volume":"7","author":"Yang Junfeng","year":"2006","unstructured":"Junfeng Yang, Can Sar, and Dawson Engler. 2006. EXPLODE: A Lightweight, General System for Finding Serious Storage System Errors. In Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation - Volume 7 (OSDI '06). USENIX Association, Berkeley, CA, USA, 10--10."},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1189256.1189259"}],"event":{"name":"ICSE '20: 42nd International Conference on Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","KIISE Korean Institute of Information Scientists and Engineers","IEEE CS"],"location":"Seoul South Korea","acronym":"ICSE '20"},"container-title":["Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3377811.3380350","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,14]],"date-time":"2024-07-14T23:19:52Z","timestamp":1720999192000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3377811.3380350"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,27]]},"references-count":69,"alternative-id":["10.1145\/3377811.3380350","10.1145\/3377811"],"URL":"https:\/\/doi.org\/10.1145\/3377811.3380350","relation":{},"subject":[],"published":{"date-parts":[[2020,6,27]]},"assertion":[{"value":"2020-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}