References

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

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org