Formalising Filesystems in the ACL2 Theorem Prover:
an Application to FAT32

Mihir Parang Mehta
ACL2 Seminar
Oct. 26, 2018

This is a practice talk for a presentation to be given at the upcoming
ACL2 Workshop.  The abstract, quoted from the paper, is as follows.

.....

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.