Name
Abstract | ||
|---|---|---|
We present an approach to writing and formally verifying high-assurance file-system code in a restricted language called Cogent, supported by a certifying compiler that produces C code, high-level specification of Cogent, and translation correctness proofs. The language is strongly typed and guarantees absence of a number of common file system implementation errors. We show how verification effort is drastically reduced for proving higher-level properties of the file system implementation by reasoning about the generated formal specification rather than its low-level C code. We use the framework to write two Linux file systems, and compare their performance with their native C implementations.
|
Year | DOI | Venue |
|---|---|---|
2016 | 10.1145/2980024.2872404 | Architectural Support for Programming Languages and Operating Systems |
Keywords | Field | DocType |
co-generation,domain-specific languages,file systems,isabelle/hol,verification | Domain-specific language,File system,Programming language,Correctness proofs,Computer science,Parallel computing,Implementation,Compiler,Formal specification,Class implementation file,High assurance | Conference |
Volume | Issue | ISSN |
44 | 2 | 0163-5964 |
Citations | PageRank | References |
19 | 0.74 | 29 |
Authors | ||
15 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sidney Amani | 1 | 67 | 5.00 |
| Alex Hixon | 2 | 19 | 0.74 |
| Zilin Chen | 3 | 19 | 0.74 |
| Christine Rizkallah | 4 | 75 | 14.05 |
| Peter Chubb | 5 | 107 | 3.81 |
| Liam O'Connor | 6 | 44 | 5.02 |
| Joel Beeren | 7 | 19 | 0.74 |
| Yutaka Nagashima | 8 | 19 | 0.74 |
| Japheth Lim | 9 | 40 | 2.95 |
| Thomas Sewell | 10 | 914 | 37.60 |
| Joseph Tuong | 11 | 19 | 0.74 |
| Gabriele Keller | 12 | 657 | 36.02 |
| Toby Murray | 13 | 242 | 17.03 |
| Gerwin Klein | 14 | 1450 | 87.47 |
| Gernot Heiser | 15 | 2525 | 137.42 |