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...

Descripción completa

Detalles Bibliográficos

Publicado en:	Communications of the ACM Vol. 60; no. 4; pp. 75 - 85
Autores principales:	Chajed, Tej, Haogang Chen, Chlipala, Adam, Kaashoek, M. Frans, Zeldovich, Nickolai, Ziegler, Daniel
Formato:	Artículo
Publicado:	Association for Computing Machinery Apr2017
Materias:	Electronic file management Hoare logic Computer system failures Information storage & retrieval systems Automation Errors
Acceso en línea:	Ver este registro en EBSCOhost