Using Crash Hoare logic for certifying the FSCQ file system
FSCQ is the first file system with a machine-checkable proof (using the Coq proof assistant) that its implementation meets its specification and whose specification includes crashes. FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient...
| Main Authors: | , , , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
Association for Computing Machinery (ACM),
2021-11-04T19:49:05Z.
|
| Subjects: | |
| Online Access: | Get fulltext |