Пост канала

Программисты РФ

1. 31.07 · 14:48фото

   Даже верифицированный компилятор может допускать ошибки. В 2011 году исследователи тестировали CompCert с использованием случайно сгенерированных C-программ и обнаружили ошибку "wrong-code" в следующем выражении: return -1 <= (1 && x); Правильный ответ — 1, но CompCert 1.6 для PowerPC выдал 0. Ошибка оказалась не в корректном оптимизаторе, а в неверифицированном фронтенде. Формальная верификация защищает только те части системы, для которых есть доказательства.

   Открыть в MAX

   Просмотры

   4 036

   ER

   2,2%

   Реакции

   89