CompCert
CompCert 3.14
正式に検証されたCコンパイラ。
Compcert C Verified Compilerは、PowerPC、ARM、X86、RISC-Vプロセッサのコードを生成するCプログラミング言語の大規模なサブセットのコンパイラです。
COMPCERTの際立った特徴は、COQプルーフアシスタントを使用して正式に検証されていることです。生成されたアセンブリコードは、ソースCコードのセマンティクスで規定されているように動作することが正式に保証されています。
COMPCERT（サポートされているプラットフォーム、サポートされているC機能、インストール手順、コンパイラの使用など）の詳細については、Webサイト、特にユーザーマニュアルを参照してください。
Compcertはフリーソフトウェアではありません。この非営利のリリースは、評価、研究、教育的、個人的な目的にのみ使用できます。この制限がなく、専門的なサポートと追加機能を備えたCOMPCERTの商用バージョンは、Absintから購入できます。詳細については、ファイルLICENSEを参照してください。
Compcert検証済みのコンパイラは、National de Recherche en Informatique et En Automatique（INRIA）およびAngewandte Informatik Gmbhです。
compcertに関する一般的な議論は、[email protected]メーリングリストで行われます。
Compcertの商用版に関するお問い合わせについては、[email protected]にお問い合わせください
