Trustworthy Systems

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

Data61
CSIRO

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,
    address          = {Nancy, France},
    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},
    booktitle        = {International Conference on Interactive Theorem Proving},
    month            = aug,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/9273.pdf},
    title            = {A Framework for the Automatic Formal Verification of Refinement from {Cogent} to {C}},
    year             = {2016}
  }

Download