Paper Info
Title
POSIX file store in Z/Eves: an experiment in the verified software repository
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 & 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.
Year
DOI
Venue
2009
10.1109/ICECCS.2007.36
Sci. Comput. Program.
Keywords
DocType
Volume
software repository,posix-compliant file store,international verification grand challenge,experiments reusable,pilot project,eves theorem prover,posix file store,unix filing system,overall objective,general theory,different domain,file store,concrete,programming,computer science,theorem proving,fault tolerance,application software,space flight,formal specification,unix,theorem prover,hardware
Journal
74
Issue
ISBN
Citations 
4
0-7695-2895-3
24
PageRank 
References 
Authors
1.06
7
3
Name
Order
Citations
PageRank
Leo Freitas11099.09
Zheng Fu2241.06
Jim Woodcock324418.34