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, Chen, Haogang, Chlipala, Adam, Kaashoek, M. Frans, Zeldovich, Nickolai, Ziegler, Daniel Todd
Other Authors: Massachusetts Institute of Technology. Laboratory for Computer Science
Format: Article
Language:English
Published: Association for Computing Machinery (ACM) 2019
Online Access:https://hdl.handle.net/1721.1/122622

Internet

https://hdl.handle.net/1721.1/122622

Similar Items