A formally verified compiler back-end Export

@article{citeulike:4044077, abstract = {This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a verified compiler is useful in the context of formal methods applied to the certification of critical software: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.}, archivePrefix = {arXiv}, author = {Leroy, Xavier}, citeulike-article-id = {4044077}, citeulike-linkout-0 = {http://arxiv.org/abs/0902.2137}, citeulike-linkout-1 = {http://arxiv.org/pdf/0902.2137}, eprint = {0902.2137}, keywords = {computation, functional, languages}, month = {Feb}, posted-at = {2009-02-13 18:25:49}, priority = {2}, title = {A formally verified compiler back-end}, url = {http://arxiv.org/abs/0902.2137}, year = {2009} }

TY - JOUR ID - citeulike:4044077 L3 - citeulike-article-id:4044077 N2 - This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a verified compiler is useful in the context of formal methods applied to the certification of critical software: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well. TI - A formally verified compiler back-end KW - computation KW - functional KW - languages AU - Leroy, Xavier PY - 2009/Feb/12/ UR - http://arxiv.org/abs/0902.2137 ER -