File System Formalizations and Verifications

This is a joint project with M.I. Lali.

Formalizing a Hierarchical File System

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.

The final paper of this project is: W.H. Hesselink, M.I. Lali: Formalizing a hierarchical file system. Formal Aspects of Computing 24 (2012) 27-44. DOI: 10.1007/s00165-010-0171-2. Here, files and directories are distinguished from the outset. A new PVS proof script is available.

Formal Verification of Cyclic Data Distribution for Parallel File Systems

A paper is being prepared. A PVS proof script is available.

Comments and questions are welcome.
Back to my home page.
Wim H. Hesselink