Categories: filesystems

Filesystems

With others, I am working on formally specifying and verifying filesystems.

SibylFS

So far, we have constructed a filesystem test oracle called SibylFS. The main page for SibylFS is here

ImpFS

We are working on a verified filesystem implementation, including a CoW B-tree library.

A recent poster talking about the different components is:

Many of these components are available from GitHub:

Note that these components in turn require other libraries (which are also available from GitHub).

A very simple set of commands to build many of these components (not path_resolution or mini-fs) is: https://github.com/tomjridge/tjr_imp_build_script

A collection of all ocamldoc documentation is: https://tomjridge.github.io/tjr_imp_build_script/


Related posts: