Categories: filesystems


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


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


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).

Related articles:

  • 2018-05-30 Potential improvements in filesystem performance
  • 2017-09-06 OCaml workshop talk: A B-tree library for OCaml
  • 2017-06-13 Interesting article on ext4 free space allocation
  • 2017-05-30 OCaml workshop submission: A B-tree library for OCaml
  • 2017-03-16 tjr-btree: a CoW B-tree library in OCaml
  • 2016-05-27 Visit to Cambridge, for REMS workshop
  • 2016-01-27 Talk at York University
  • 2015-10-05 SibylFS presentation at SOSP'15
  • 2015-09-28 SibylFS SOSP poster
  • 2015-09-21 SibylFS presentation to Industrial Advisory Board
  • 2015-06-28 SOSP 2015 paper acceptance for SibylFS
  • 2015-04-21 REMS Cambridge talk on SibylFS
  • 2013-11-13 Engineer position
  • 2013-04-01 PhD position funded by Microsoft Research
  • 2013-02-01 EPSRC grant funded