Certifying a File System Using Crash Hoare Logic: Correctness in the Presence of Crashes.

FSCQ is the first file system with a machine-checkable proof that its implementation meets a specification, even in the presence of fail-stop crashes. FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient barriers or forgetting to zero o...

Full description

Bibliographic Details

Published in:	Communications of the ACM Vol. 60; no. 4; pp. 75 - 85
Main Authors:	Chajed, Tej, Haogang Chen, Chlipala, Adam, Kaashoek, M. Frans, Zeldovich, Nickolai, Ziegler, Daniel
Format:	Article
Published:	Association for Computing Machinery Apr2017
Subjects:	Electronic file management Hoare logic Computer system failures Information storage & retrieval systems Automation Errors
Online Access:	View this record in EBSCOhost