Name
Abstract | ||
|---|---|---|
Our language Cogent simplifies verification of systems software using a certifying compiler, which produces a proof that the generated C code is a refinement of the original Cogent program. Despite the fact that Cogent itself contains a number of refinement layers, the semantic gap between even the lowest level of Cogent semantics and the generated C code remains large.In this paper we close this gap with an automated refinement framework which validates the compiler's code generation phase. This framework makes use of existing C verification tools and introduces a new technique to relate the type systems of Cogent and C. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-319-43144-4_20 | INTERACTIVE THEOREM PROVING (ITP 2016) |
Field | DocType | Volume |
Programming language,Computer science,Semantic gap,Algorithm,Compiler,Software,Semantics,Formal verification | Conference | 9807 |
ISSN | Citations | PageRank |
0302-9743 | 3 | 0.39 |
References | Authors | |
8 | 9 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christine Rizkallah | 1 | 75 | 14.05 |
| Japheth Lim | 2 | 40 | 2.95 |
| Yutaka Nagashima | 3 | 23 | 6.13 |
| Thomas Sewell | 4 | 914 | 37.60 |
| Zilin Chen | 5 | 23 | 2.53 |
| Liam O'Connor | 6 | 44 | 5.02 |
| Toby Murray | 7 | 242 | 17.03 |
| Gabriele Keller | 8 | 657 | 36.02 |
| Gerwin Klein | 9 | 1450 | 87.47 |