loading...
 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 -
 
Leo Freitas, University of York, UK
Zheng Fu, University of York, UK
Jim Woodcock, University of York, UK
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.