Formal verification of a C-Compiler frontend.

Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy has written Formal verification of a C-Compiler frontend. Some previous work is already mentioned on LtU here. Abstract:

This paper presents the formal verification of a compiler front-end that translates a subset of the C language into the Cminor intermediate language. The semantics of the source and target languages as well as the translation between them have been written in the speci- fication language of the Coq proof assistant. The proof of observational semantic equivalence between the source and generated code has been machine-checked using Coq. An executable compiler was obtained by automatic extraction of executable Caml code from the Coq specification of the translator, combined with a certified compiler back-end generating PowerPC assembly code from Cminor, described in previous work.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Direct link to the previous

Direct link to the previous discussion.