| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 434216 | Science of Computer Programming | 2009 | 20 Pages |
Abstract
We present results from the second pilot project in the international Verification Grand Challenge: a formally verified specification of a POSIX-compliant file store using the Z/Eves theorem prover. The project’s overall objective is to build a verified file store for space-flight missions. Our specification of the file store is based on Morgan and Sufrin’s specification of the UNIX filing system; the proof and its mechanisation in Z/Eves are novel. We show how our work contributes towards building a verified software repository: a set of general theories, proof techniques, and experiments reusable across different domains.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
