コンプサート

CompCertは、 C99プログラミング言語（Clightとして知られる）の大規模なサブセット用の形式検証済みの最適化コンパイラであり、現在はPowerPC、ARM、RISC-V、x86、x86-64 ^[3]アーキテクチャを対象としています。^[4] Xavier Leroyが率いるこのプロジェクトは、フランスの研究所ANRとINRIAの資金提供を受けて2005年に正式に開始されました。コンパイラはCoqで仕様が規定され、プログラムされ、実証されています。信頼性が求められる組み込みシステムのプログラミングに使用することを目的としています。生成されたコードのパフォーマンスは、最適化レベル-O1のGCC （バージョン3）のパフォーマンスに近いことが多く、最適化なしのGCCのパフォーマンスよりも常に優れています。^[5]

2015年以来、AbsIntは商用ライセンスを提供し、^[6]サポートとメンテナンスを提供し、ツールの進歩に貢献しています。CompCertは非商用​​ライセンスでリリースされているため、フリーソフトウェアではありませんが、一部のソースファイルはGNU Lesser General Public Licenseバージョン2.1以降とのデュアルライセンスであるか、他のライセンスの条件で利用可能です。^[2]

複数の商用アーキテクチャをターゲットとし、その正しさが完全に機械的にチェックされた証明を持つ初の実用的な最適化コンパイラである CompCert の開発により、Xavier Leroyと CompCert の開発チームは 2021 ACM ソフトウェア システム賞を受賞しました。

• 公式サイト
• GitHub上の CompCert
• 現実的なコンパイラの形式検証
• ソフトウェア システム賞 — ACM アワード