Certifying a file system using crash hoare logic

Certifying a file system using crash hoare logic

FSCQ is the frst fle system with a machine-checkable proof that its implementation meets a specifcation, even in the presence of fail-stop crashes. FSCQ provably avoids bugs that have plagued previous fle systems, such as performing disk writes without suffcient barriers or forgetting to zero out di...

Full description

Bibliographic Details
Main Authors: Chajed, Tej (Author), Chen, Haogang (Author), Chlipala, Adam (Author), Kaashoek, M. Frans (Author), Zeldovich, Nickolai (Author), Ziegler, Daniel Todd (Author)
Other Authors: Massachusetts Institute of Technology. Laboratory for Computer Science (Contributor), Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory (Contributor), Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science (Contributor)
Format: Article
Language:English
Published: Association for Computing Machinery (ACM), 2019-10-18T13:28:41Z.
Subjects:
Article
Online Access:Get fulltext

Internet

Get fulltext

Similar Items