Inside a Verified Flash File System: Transactions & Garbage Collection

With the work presented here we address a long-standing conceptual gap in flash file system verification: We map an abstract graph-based representation down to the flat blocks of bytes of the storage medium. Specifically, we consider grouping of file system objects into atomic transactions together with layout, allocation and garbage collection of on-flash storage space. Two major concerns guide the design and verification: proper handling of errors and, more importantly, guaranteed recovery from unexpected power-cuts. Finding useful specifications of intermediate interfaces to address these concerns realistically dominates the verification effort.
published 2015 Proc. of 7th Working Conference on Verified Software: Theories, Tools and Experiments

Publisher: Springer


The final publication is available at Springer via

For questions regarding the publication, please contact!