Bilby File System
| Description: | Bilby Filesystem (BilbyFs), a Linux flash file system |
| Author(s): | Sidney Armani, Toby Murray |
| Event(s): | MARS'15 |
| Paper(s): |
Specifying a Realistic File System |
Abstract
We present the most interesting elements of the correctness specification of BilbyFs, a performant Linux flash file system. The BilbyFs specification supports asynchronous writes, a feature that has been overlooked by several file system verification projects, and has been used to verify the correctness of BilbyFs's fsync() C implementation. It makes use of nondeterminism to be concise and is shallowly-embedded in higher-order logic.
Model(s)
-
- Download Model
- Browse Model
- tool(s): Isabelle/HOL
This work is licensed under a Creative Commons
Attribution-NonCommercial-ShareAlike 4.0 International License.