References

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