Development of a Verified Flash File System

Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Dominik Haneberg, Wolfgang Reif

This paper gives an overview over the development of a formally verified file system for flash memory. We describe our approach that is based on Abstract State Machines and incremental modular refinement. Some of the important intermediate levels and the features they introduce are given. We report on the verification challenges addressed so far, and point to open problems and future work. We furthermore draw preliminary conclusions on the methodology and the required tool support.
published 2014 Proc. of 4th International Conference ABZ 2014

Publisher: Springer

DOI: (Springer Link)


The final publication is available at Springer via

For questions regarding the publication, please contact!