Skip to main content


A framework for the automatic formal verification of refinement from Cogent to C


Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby Murray, Gabriele Keller and Gerwin Klein




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.

BibTeX Entry

    author           = {Rizkallah, Christine and Lim, Japheth and Nagashima, Yutaka and Sewell, Thomas and Chen, Zilin and
                        O'Connor, Liam and Murray, Toby and Keller, Gabriele and Klein, Gerwin},
    month            = {aug},
    year             = {2016},
    title            = {A Framework for the Automatic Formal Verification of Refinement from {Cogent} to {C}},
    booktitle        = {International Conference on Interactive Theorem Proving},
    address          = {Nancy, France}