CompCert
CompCert 3.14
正式驗證的C編譯器。
CompCert C驗證的編譯器是C編程語言的大量子集的編譯器，可為PowerPC，ARM，X86和RISC-V處理器生成代碼。
CompCert的區別特徵是它已使用COQ證明助手進行了正式驗證：生成的彙編代碼可以正式保證按照源C代碼的語義規定的規定。
有關COMPCERT（支持的平台，支持的C功能，安裝說明，使用編譯器等）的更多信息，請參閱網站，尤其是用戶手冊。
CompCert不是免費軟件。此非商業版本只能用於評估，研究，教育和個人目的。可以從ABSINT購買商業版的CompCert，沒有這種限制，沒有專業支持和額外功能。有關更多信息，請參見文件LICENSE 。
經過驗證的編譯器是版權所有Informatique et Automatique（Inria）和Absint Angewandte Informatik GmbH。
關於CompCert的一般討論在[email protected]郵件列表上進行。
有關Compcert商業版本的查詢，請聯繫[email protected]
