This is a joint project with M.I. Lali.
Appeared has: W.H. Hesselink, M.I. Lali: Formalizing a Hierarchical File System. Electronic Notes in Theoretical Computer Science 259 (2009) 67--85, Proceedings of the 14th BCS-FACS Refinement Workshop (REFINE 2009). A PVS proof script is available. For inspection, you need to have PVS. First gunzip the file, then in PVS call "undump" on the result. This gives files with the extension "pvs", which can be inspected, and proved by PVS.
We are preparing an extended version that distinguishes files and directories from the outset. A new PVS proof script is available.
A paper is being prepared. A PVS proof script is available.
Comments and questions are welcome.
Back to my home page.
Wim H. Hesselink