We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.
We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.
from IV - Operational semantics of CompCert
Published online by Cambridge University Press: 05 August 2014
Program logics for certified compilers: We prove that the program logic is sound with respect to the operational semantics of a source language—meaning that if the program logic proves some claim about the observable behavior of a program, then the source program actually respects that claim when interpreted in the source-language semantics. But computers don't directly execute source-language semantics: we also need a proof about the correctness of an interpreter or a compiler.
CompCert (compilateur certifié in French) is a formally verified optimizing compiler for the C language, translating to assembly language for various machines (Intel x86, ARM, PowerPC) [62]. Like most optimizing compilers, it translates in several sequential phases through a sequence of intermediate languages. Unlike most compilers, each of these intermediate languages has a formal specification written down in Coq as an operational semantics. Each phase is proved correct: the form of the proof is a simulation theorem expressing that the observable behavior of the target program corresponds to the observable behavior of the source program. The composition of all these per-phase simulation theorems gives the compiler correctness theorem.
Although there had been formally verified compilers before [67, 36, 61, 60], CompCert is an important breakthrough for several reasons:
Language: One of Leroy's goals has been that CompCert should be able to compile real high-assurance embedded C programs, such as the avionics software for a commercial jetliner. Such software is not trivially modified: any tweak to the software—let alone rewriting it in another language—requires months or years of rebuilding an assurance case.
To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.
Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.
Find out more about the Kindle Personal Document Service.
To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.
To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.
