CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler

CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler
复制标题

CompCert：集成和鉴定经过形式验证的优化编译器的实践经验

DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Sandrine Blazy
Sandrine Blazy
中科院分区：
--
文献类型：
--
作者：
Daniel Kästner;J. Barrho;Ulrich Wünsche;Marc Schlickling;Bernhard Schommer;Michael Schmidt;C. Ferdinand;X. Leroy;Sandrine Blazy

文献摘要

被引文献

相似文献

CompCert是第一个商业上可用的优化编译器，使用机器辅助数学证明进行正式验证，以避免错误编译。它产生的可执行代码被证明完全符合源C程序的语义。本文概述了如何使用CompCert为高度安全关键的行业应用获得认证积分，并根据IEC 60880进行认证。我们将简要介绍目标应用程序，说明将现有编译器基础结构更改为CompCert的过程，并讨论性能特征。主要部分集中在工具鉴定策略，特别是如何利用形式的正确性证明在认证过程中。
CompCert is the first commercially available optimizing compiler that is formally verified, using machine-assisted mathematical proofs, to be exempt from mis-compilation. The executable code it produces is proved to behave exactly as specified by the semantics of the source C program. This article gives an overview of the use of CompCert to gain certification credits for a highly safety-critical industry application, certified according to IEC 60880. We will briefly introduce the target application, illustrate the process of changing the existing compiler infrastructure to CompCert, and discuss performance characteristics. The main part focuses on the tool qualification strategy, in particular on how to take advantage of the formal correctness proof in the certification process.