Verifying a File System Implementation

paper ps   
We present a correctness proof for a basic file system implementation. This implementation contains key elements of standard Unix file systems such as inodes and fixed-size disk blocks. We prove the implementation correct by establishing a simulation relation between the specification of the file system (which models the file system as an abstract map from file names to sequences of bytes) and its implementation (which uses fixed-size disk blocks to store the contents of the files). We used the Athena proof system to represent and validate our proof. Our experience indicates that Athena's use of block-structured natural deduction, support for structural induction and proof abstraction, and seamless integration with high-performance automated theorem provers were essential to our ability to successfully manage a proof of this size.

Citation

Konstantine Arkoudas, Karen Zee, Viktor Kuncak, and Martin Rinard. Verifying a file system implementation. In Sixth International Conference on Formal Engineering Methods, volume 3308 of LNCS, Seattle, 2004. See also technical report [25].

BibTex Entry

@inproceedings{ArkoudasETAL04VerifyingFileSystemImplementationICFEM,
  author = {Konstantine Arkoudas and Karen Zee and Viktor Kuncak and Martin Rinard},
  title = {Verifying a File System Implementation},
  booktitle = {Sixth International Conference on Formal Engineering Methods},
  year = 2004,
  address = {Seattle},
  series = {LNCS},
  volume = {3308},
  note = {See also technical report
          \cite{ArkoudasETAL04VerifyingFileSystemImplementationICFEM}},
  abstract = {
We present a correctness proof for a basic file system
implementation. This implementation contains key elements of standard
Unix file systems such as inodes and fixed-size disk blocks.  We prove
the implementation correct by establishing a simulation relation
between the specification of the file system (which models the file
system as an abstract map from file names to sequences of bytes) and
its implementation (which uses fixed-size disk blocks to store 
the contents of the files). 
We used the Athena proof system to represent and validate our proof.
Our experience indicates that Athena's use of block-structured natural 
deduction, support for structural induction and proof 
abstraction, and  seamless integration with high-performance automated theorem
provers were essential to our ability to successfully manage a proof of
this size. 
}
}