@article(abadi1991existence,
 author       = {Mart{\'\i}n Abadi and Leslie Lamport},
 year         = {1991},
 title        = {The existence of refinement mappings},
 journal      = {Theoretical Computer Science},
 volume       = {82},
 number       = {2},
 pages        = {253--284},
 doi          = {10.1016/0304-3975(91)90224-P},
)
@inproceedings(amani2016cogent,
 author       = {Sidney Amani and Alex Hixon and Zilin Chen and Christine Rizkallah and Peter Chubb and Liam O'Connor and Joel Beeren and Yutaka Nagashima and Japheth Lim and Thomas Sewell},
 year         = {2016},
 title        = {Cogent: Verifying high-assurance file system implementations},
 booktitle    = {ACM SIGPLAN Notices},
 volume       = {51},
 organization = {ACM},
 pages        = {175--188},
 doi          = {10.1145/2872362.2872404},
)
@book(bertot2013interactive,
 author       = {Yves Bertot and Pierre Cast{\'e}ran},
 year         = {2013},
 title        = {Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions},
 publisher    = {Springer Science \& Business Media},
 doi          = {10.1007/978-3-662-07964-5},
)
@techreport(bevier1996executable,
 author       = {William R. Bevier and Richard M. Cohen},
 year         = {1996},
 title        = {An executable model of the Synergy file system},
 type         = {Technical Report},
 institution  = {Technical Report 121, Computational Logic, Inc},
)
@inproceedings(boyer2002single,
 author       = {Robert S. Boyer and J Strother Moore},
 year         = {2002},
 title        = {Single-threaded objects in ACL2},
 booktitle    = {International Symposium on Practical Aspects of Declarative Languages},
 organization = {Springer},
 pages        = {9--27},
 doi          = {10.1007/3-540-45587-6\_3},
)
@inproceedings(DBLP:conf/usenix/ChenZCCKZ16,
 author       = {Haogang Chen and Daniel Ziegler and Tej Chajed and Adam Chlipala and M. Frans Kaashoek and Nickolai Zeldovich},
 year         = {2016},
 title        = {Using Crash Hoare Logic for Certifying the {FSCQ} File System},
 editor       = {Ajay Gulati and Hakim Weatherspoon},
 booktitle    = {2016 {USENIX} Annual Technical Conference, {USENIX} {ATC} 2016, Denver, CO, USA, June 22-24, 2016.},
 publisher    = {{USENIX} Association},
 doi          = {10.1145/2815400.2815402},
 url          = {https://www.usenix.org/conference/atc16},
)
@article(cox6xv6,
 author       = {Russ Cox and M. Frans Kaashoek and Robert T. Morris},
 title        = {Xv6, a simple Unix-like teaching operating system, 2016},
 url          = {http://pdos.csail.mit.edu/6.828/2014/xv6.html},
)
@inproceedings(de2008z3,
 author       = {De Moura, Leonardo and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {Z3: An efficient SMT solver},
 booktitle    = {International conference on Tools and Algorithms for the Construction and Analysis of Systems},
 organization = {Springer},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3\_24},
)
@misc(eggertdiff,
 author       = {Paul Eggert and Mike Haertel and David Hayes and Richard Stallman and Len Tower},
 title        = {diff (1)-Linux manual page, accessed: 07 Sep 2018},
)
@article(goel2013abstract,
 author       = {Shilpi Goel and Hunt Jr., Warren A. and Matt Kaufmann},
 year         = {2013},
 title        = {Abstract stobjs and their application to ISA modeling},
 journal      = {arXiv preprint arXiv:1304.7858},
 doi          = {10.4204/EPTCS.114.5},
)
@inproceedings(goel2014simulation,
 author       = {Shilpi Goel and Hunt Jr., Warren A. and Matt Kaufmann and Soumava Ghosh},
 year         = {2014},
 title        = {Simulation and formal verification of x86 machine-code programs that make system calls},
 booktitle    = {Formal Methods in Computer-Aided Design (FMCAD), 2014},
 organization = {IEEE},
 pages        = {91--98},
 doi          = {10.1109/FMCAD.2014.6987600},
)
@misc(granlundcp,
 author       = {Torbjorn Granlund and David MacKenzie and Jim Meyering},
 title        = {cp (1)-Linux manual page, accessed: 09 Jul 2018},
)
@misc(hudsonmkfs,
 author       = {Dave Hudson and Peter Anvin and Roman Hodek},
 title        = {mkfs.fat (8)-Linux manual page, accessed: 09 Jul 2018},
)
@book(kaufmann2000,
 author       = {Matt Kaufmann and Panagiotis Manolios and J Strother Moore},
 year         = {2000},
 title        = {Computer-aided reasoning: an approach},
 publisher    = {Kluwer Academic Publishers},
 doi          = {10.1007/978-1-4757-3188-0},
)
@misc(kerriskclose,
 author       = {Michael Kerrisk},
 title        = {close (2)-Linux manual page, accessed: 09 Jul 2018},
)
@misc(kerriskerrno,
 author       = {Michael Kerrisk},
 title        = {errno (3)-Linux manual page, accessed: 07 Sep 2018},
)
@misc(kerrisklstat,
 author       = {Michael Kerrisk},
 title        = {lstat (2)-Linux manual page, accessed: 09 Jul 2018},
)
@misc(kerriskmkdir,
 author       = {Michael Kerrisk},
 title        = {mkdir (2)-Linux manual page, accessed: 09 Jul 2018},
)
@misc(kerriskmknod,
 author       = {Michael Kerrisk},
 title        = {mknod (2)-Linux manual page, accessed: 09 Jul 2018},
)
@misc(kerriskopen,
 author       = {Michael Kerrisk},
 title        = {open (2)-Linux manual page, accessed: 09 Jul 2018},
)
@misc(kerriskpread,
 author       = {Michael Kerrisk},
 title        = {pread (2)-Linux manual page, accessed: 09 Jul 2018},
)
@misc(kerriskpwrite,
 author       = {Michael Kerrisk},
 title        = {pwrite (2)-Linux manual page, accessed: 09 Jul 2018},
)
@inproceedings(klein2009sel4,
 author       = {Gerwin Klein and Kevin Elphinstone and Gernot Heiser and June Andronick and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish},
 year         = {2009},
 title        = {seL4: Formal verification of an OS kernel},
 booktitle    = {Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles},
 organization = {ACM},
 pages        = {207--220},
 doi          = {10.1145/1629575.1629596},
)
@inproceedings(mathur2007new,
 author       = {Avantika Mathur and Mingming Cao and Suparna Bhattacharya and Andreas Dilger and Alex Tomas and Laurent Vivier},
 year         = {2007},
 title        = {The new ext4 filesystem: current status and future plans},
 booktitle    = {Proceedings of the Linux symposium},
 volume       = {2},
 pages        = {21--33},
)
@misc(microsoft2000,
 author       = {Microsoft},
 year         = {2000},
 title        = {Microsoft Extensible Firmware Initiative FAT32 File System Specification},
 url          = {https://download.microsoft.com/download/1/6/1/161ba512-40e2-4cc9-843a-923143f3456c/fatgen103.doc},
)
@misc(moriacpm,
 author       = {Michael Moria},
 title        = {cpm (5)-Linux manual page, accessed: 07 Sep 2018},
)
@inproceedings(Nelson:2017:HPV:3132747.3132748,
 author       = {Luke Nelson and Helgi Sigurbjarnarson and Kaiyuan Zhang and Dylan Johnson and James Bornholt and Emina Torlak and Xi Wang},
 year         = {2017},
 title        = {Hyperkernel: Push-Button Verification of an OS Kernel},
 booktitle    = {Proceedings of the 26th Symposium on Operating Systems Principles},
 series       = {SOSP '17},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {252--269},
 url          = {http://doi.acm.org/10.1145/3132747.3132748},
)
@book(nipkow2002isabelle,
 author       = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
 year         = {2002},
 title        = {Isabelle/HOL: a proof assistant for higher-order logic},
 volume       = {2283},
 publisher    = {Springer Science \& Business Media},
 doi          = {10.1007/3-540-45949-9},
)
@inproceedings(ridge2015sibylfs,
 author       = {Tom Ridge and David Sheets and Thomas Tuerk and Andrea Giugliano and Anil Madhavapeddy and Peter Sewell},
 year         = {2015},
 title        = {SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems},
 booktitle    = {Proceedings of the 25th Symposium on Operating Systems Principles},
 organization = {ACM},
 pages        = {38--53},
 doi          = {10.1145/2815400.2815411},
)
@inbook(lkmpgchap4,
 author       = {Peter Jay Salzman and Ori Pomerantz},
 year         = {2001},
 title        = {The Linux Kernel Module Programming Guide},
 chapter      = {4},
 url          = {https://www.tldp.org/LDP/lkmpg/2.4/html/c577.htm},
)
@inproceedings(sigurbjarnarson2016push,
 author       = {Helgi Sigurbjarnarson and James Bornholt and Emina Torlak and Xi Wang},
 year         = {2016},
 title        = {Push-Button Verification of File Systems via Crash Refinement.},
 booktitle    = {OSDI},
 volume       = {16},
 pages        = {1--16},
 url          = {https://www.usenix.org/conference/atc17/technical-sessions/presentation/sigurbjarnarson},
)
@inproceedings(15-swords-fty,
 author       = {Sol Swords and Jared Davis},
 year         = {2015},
 title        = {Fix Your Types},
 booktitle    = {Proceedings of the Thirteenth International Workshop on the {ACL2} Theorem Prover and its Applications ({ACL2} '15)},
 doi          = {10.4204/EPTCS.192.2},
)