Verifying a file system implementation
Konstantine Arkoudas, Karen Zee, Viktor Kuncak, and Martin Rinard
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.
BibTeX Entry
@InProceedings{ArkoudasETALICFEM2004VerifyingFileSystemImplementation,
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 (ICFEM'04)},
series = {Lecture Notes in Computer Science (LNCS)},
volume = {3308},
pages = {373-390},
year = {2004},
address = {Seattle},
month = {November 2004}
}
Back to the
publication list of Konstantine Arkoudas