CompCert — проект по созданию официально верифицированных компиляторов. В рамках проекта разработан компилятор CompCert C для языка Си (стандартов ISO C90 / ANSI C с некоторыми незначительными ограничениями и отдельными расширениями, вдохновлённые последующими стандартами), а также полностью написана и продемонстрирована система верификации Coq . Основной разработчик — Ксавье Леруа . У этого компилятора есть машинная проверка того, что сгенерированный код ведёт себя так же, как и исходный код. Компилятор позволяет генерировать машинный код для архитектур процессора PowerPC , ARM и x86 .

Код, сгенерированный CompCert, примерно вдвое быстрее, чем сгенерированный GCC без оптимизации и немного медленнее, чем сгенерированный с более высокими уровнями оптимизации

См. также

• Формальная верификация
• Формальные методы

Примечания

Ссылки