A Framework For The Automatic Formal Verification Of Refinement From Cogent To C

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.