@techreport(Bevier_CT_95,
 author       = {William Bevier and Richard Cohen and Jeff Turner},
 year         = {1995},
 title        = {A Specification for the {Synergy} File System},
 type         = {Technical Report},
 number       = {Technical Report 120},
 institution  = {Computational Logic Inc.},
 address      = {Austin, Texas, USA},
 url          = {http://computationallogic.com/reports/files/120.pdf},
)
@inproceedings(Chen_ZCCKZ_15,
 author       = {Haogang Chen and Daniel Ziegler and Tej Chajed and Adam Chlipala and M. Frans Kaashoek and Nickolai Zeldovich},
 year         = {2015},
 title        = {Using {Crash} {Hoare} Logic for Certifying the {FSCQ} File System},
 address      = {Monterey, CA},
 doi          = {10.1145/2815400.2815402},
 note         = {To appear},
)
@inproceedings(Cock_KS_08,
 author       = {David Cock and Gerwin Klein and Thomas Sewell},
 year         = {2008},
 title        = {Secure Microkernels, State Monads and Scalable Refinement},
 booktitle    = {21st TPHOLs},
 address      = {Montreal, Canada},
 pages        = {167--182},
 doi          = {10.1007/978-3-540-71067-7\_16},
)
@article(Ernst_SHPR_12,
 author       = {Gidon Ernst and Gerhard Schellhorn and Dominik Haneberg and J{\"o}rg Pf{\"a}hler and Wolfgang Reif},
 year         = {2012},
 title        = {A formal model of a virtual filesystem switch},
 journal      = {arXiv preprint arXiv:1211.6187},
 doi          = {10.4204/EPTCS.102.5},
)
@inproceedings(Ernst_SHPR_13,
 author       = {Gidon Ernst and Gerhard Schellhorn and Dominik Haneberg and J{\"{o}}rg Pf{\"{a}}hler and Wolfgang Reif},
 year         = {2013},
 title        = {Verification of a Virtual Filesystem Switch},
 booktitle    = {VSTTE 2013},
 series       = {LNCS},
 volume       = {8164},
 address      = {Menlo Park, CA, USA},
 pages        = {242--261},
 doi          = {10.1007/978-3-642-54108-7\_13},
)
@inproceedings(Hesselink_Lali_09,
 author       = {Wim H. Hesselink and Muhammad Ikram Lali},
 year         = {2009},
 title        = {Formalizing a Hierarchical File System},
 booktitle    = {14th REFINE},
 series       = {ENTCS},
 volume       = {259},
 address      = {Eindhoven, The Netherlands},
 pages        = {67--85},
 doi          = {10.1016/j.entcs.2009.12.018},
)
@misc(Hunter_08,
 author       = {Adrian Hunter},
 year         = {2008},
 title        = {A brief introduction to the design of UBIFS},
)
@article(Joshi_Holzmann_07,
 author       = {Rajeev Joshi and Gerard J Holzmann},
 year         = {2007},
 title        = {A mini challenge: build a verifiable filesystem},
 journal      = {Formal Aspects of Computing},
 volume       = {19},
 number       = {2},
 pages        = {269--272},
 doi          = {10.1007/s00165-006-0022-3},
)
@article(Lu_AAL_14,
 author       = {Lanyue Lu and Arpaci-Dusseau, Andrea C. and Arpaci-Dusseau, Remzi H. and Shan Lu},
 year         = {2014},
 title        = {A Study of {Linux} File System Evolution},
 volume       = {10},
 number       = {1},
 pages        = {3:1--3:32},
 doi          = {10.1145/2560012},
)
@article(Morgan_Sufrin_84,
 author       = {Carroll Morgan and Bernard Sufrin},
 year         = {1984},
 title        = {Specification of the {UNIX} Filing System},
 journal      = {Trans. Softw. Engin.},
 volume       = {10},
 number       = {2},
 pages        = {128--142},
 doi          = {10.1109/TSE.1984.5010215},
)
@book(Nipkow_PW:Isabelle,
 author       = {Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
 year         = {2002},
 title        = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
 series       = {LNCS},
 volume       = {2283},
 doi          = {10.1007/3-540-45949-9},
)
@book(deRoever_Engelhardt:DR,
 author       = {Willem-Paul de Roever and Kai Engelhardt},
 year         = {1998},
 title        = {Data Refinement: Model-Oriented Proof Methods and their Comparison},
 volume       = {47},
 address      = {United Kingdom},
 doi          = {10.1017/CBO9780511663079},
)
@article(Thompson_78,
 author       = {Ken Thompson},
 year         = {1978},
 title        = {UNIX Time-Sharing System: UNIX Implementation},
 journal      = {Bell System Technical Journal},
 volume       = {57},
 number       = {6},
 pages        = {1931--1946},
 doi          = {10.1002/j.1538-7305.1978.tb02137.x},
)
@inproceedings(Woodhouse_03,
 author       = {David Woodhouse},
 year         = {2003},
 title        = {Jffs2: The journalling flash file system, version 2},
 booktitle    = {proceedings of Ottawa Linux Symposium},
)