A Framework for the Automatic Formal Verification of Refinement from Cogent to C

Select |




Print


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

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


2016-08-22


Conference Material


Interactive Theorem Proving


Nancy, France


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.


https://itp2016.inria.fr


nicta:9273


Rizkallah, Christine; Lim, Japheth; Nagashima, Yutaka; Sewell, Thomas; Chen, Zilin; O'Connor, Liam; Murray, Toby; Keller, Gabriele; Klein, Gerwin. A Framework for the Automatic Formal Verification of Refinement from Cogent to C. In: Interactive Theorem Proving; Nancy, France. 2016-08-22.



Loading citation data...

Citation counts
(Requires subscription to view)