POSIX file store in Z/Eves: an experiment in the verified software repository

摘要

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 & 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 and experiments reusable across different domains.