  In this work, we present an approach towards constructing executable
specifications of existing filesystems and verifying their functional
properties in a theorem proving environment. We detail an application of this
approach to the FAT32 filesystem.
  We also detail the methodology used to build up this type of executable
specification through a series of models which incrementally add features of
the target filesystem. This methodology has the benefit of allowing the
verification effort to start from simple models which encapsulate features
common to many filesystems and which are thus suitable for reuse.
