POSIX file store in Z/Eves: An experimen
โ
Leo Freitas; Jim Woodcock; Zheng Fu
๐
Article
๐
2009
๐
Elsevier Science
๐
English
โ 796 KB
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 spec