Skip to main content

TS

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

Authors

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

NICTA

UNSW

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.

BibTeX Entry

  @inproceedings{Rizkallah_LNSCOMKK_16,
    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}
  }

Download