|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
12th IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2007)
POSIX file store in Z/Eves: an experiment in the verified software repository
Auckland, New Zealand
July 11-July 14
ISBN: 0-7695-2895-3
| ASCII Text | x | ||
| Leo Freitas, Zheng Fu, Jim Woodcock, "POSIX file store in Z/Eves: an experiment in the verified software repository," Engineering of Complex Computer Systems, IEEE International Conference on, pp. 3-14, 12th IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2007), 2007. | |||
| BibTex | x | ||
| @article{ 10.1109/ICECCS.2007.36, author = {Leo Freitas and Zheng Fu and Jim Woodcock}, title = {POSIX file store in Z/Eves: an experiment in the verified software repository}, journal ={Engineering of Complex Computer Systems, IEEE International Conference on}, volume = {0}, year = {2007}, isbn = {0-7695-2895-3}, pages = {3-14}, doi = {http://doi.ieeecomputersociety.org/10.1109/ICECCS.2007.36}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - Engineering of Complex Computer Systems, IEEE International Conference on TI - POSIX file store in Z/Eves: an experiment in the verified software repository SN - 0-7695-2895-3 SP3 EP14 A1 - Leo Freitas, A1 - Zheng Fu, A1 - Jim Woodcock, PY - 2007 KW - null VL - 0 JA - Engineering of Complex Computer Systems, IEEE International Conference on ER - | |||
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.
Citation:
Leo Freitas, Zheng Fu, Jim Woodcock, "POSIX file store in Z/Eves: an experiment in the verified software repository," iceccs, pp.3-14, 12th IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.