Specifying A Realistic File System
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE(2015)
摘要
We present the most interesting elements of the correctness specification of BilbyFs, a performant Linux flash file system. The BilbyFs specification supports asynchronous writes, a feature that has been overlooked by several file system verification projects, and has been used to verify the correctness of BilbyFs's fsync () C implementation. It makes use of nondeterminism to be concise and is shallowly-embedded in higher-order logic.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络