On Verifying a File System Implementation
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 sy...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Language: | en_US |
| Published: |
2005
|
| Online Access: | http://hdl.handle.net/1721.1/30468 |
| _version_ | 1811095395025027072 |
|---|---|
| author | Arkoudas, Konstantine Zee, Karen Kuncak, Viktor Rinard, Martin |
| author2 | Computer Architecture |
| author_facet | Computer Architecture Arkoudas, Konstantine Zee, Karen Kuncak, Viktor Rinard, Martin |
| author_sort | Arkoudas, Konstantine |
| collection | MIT |
| description | 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 checker 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 connection with high-performance automated theorem provers were essential to our ability to successfully manage a proof of this size. |
| first_indexed | 2024-09-23T16:16:04Z |
| id | mit-1721.1/30468 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T16:16:04Z |
| publishDate | 2005 |
| record_format | dspace |
| spelling | mit-1721.1/304682019-04-12T08:37:47Z On Verifying a File System Implementation Arkoudas, Konstantine Zee, Karen Kuncak, Viktor Rinard, Martin Computer Architecture 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 checker 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 connection with high-performance automated theorem provers were essential to our ability to successfully manage a proof of this size. 2005-12-22T01:30:49Z 2005-12-22T01:30:49Z 2004-05-06 MIT-CSAIL-TR-2004-028 MIT-LCS-TR-946 http://hdl.handle.net/1721.1/30468 en_US Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory 31 p. 26287249 bytes 1119970 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Arkoudas, Konstantine Zee, Karen Kuncak, Viktor Rinard, Martin On Verifying a File System Implementation |
| title | On Verifying a File System Implementation |
| title_full | On Verifying a File System Implementation |
| title_fullStr | On Verifying a File System Implementation |
| title_full_unstemmed | On Verifying a File System Implementation |
| title_short | On Verifying a File System Implementation |
| title_sort | on verifying a file system implementation |
| url | http://hdl.handle.net/1721.1/30468 |
| work_keys_str_mv | AT arkoudaskonstantine onverifyingafilesystemimplementation AT zeekaren onverifyingafilesystemimplementation AT kuncakviktor onverifyingafilesystemimplementation AT rinardmartin onverifyingafilesystemimplementation |