CompCert — это официально проверенный оптимизирующий компилятор для большого подмножества языка программирования C99 (известного как Clight), который в настоящее время предназначен для архитектур PowerPC , ARM , RISC-V , x86 и x86-64 [4] . [5] Этот проект, возглавляемый Ксавье Леруа , официально стартовал в 2005 году и финансировался французскими институтами ANR и INRIA . Компилятор указан, запрограммирован и проверен в Coq . Он предназначен для использования для программирования встроенных систем, требующих надежности . Производительность сгенерированного кода часто близка к производительности GCC (версия 3) на уровне оптимизации -O1 и всегда лучше, чем у GCC без оптимизации. [6]
С 2015 года AbsInt предлагает коммерческие лицензии, [7] обеспечивает поддержку и обслуживание, а также способствует развитию инструмента. CompCert выпускается под некоммерческой лицензией и, следовательно, не является свободным программным обеспечением , хотя некоторые из его исходных файлов имеют двойную лицензию GNU Lesser General Public License версии 2.1 или более поздней или доступны на условиях других лицензий. [3]
За разработку CompCert, первого практически полезного оптимизирующего компилятора, ориентированного на несколько коммерческих архитектур и имеющего полное, механически проверенное доказательство его правильности, Ксавье Лерой и команда разработчиков CompCert получили премию ACM Software System Award 2021 .