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...
| Main Authors: | , , , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
Association for Computing Machinery (ACM)
2019
|
| Online Access: | https://hdl.handle.net/1721.1/122622 |