Исходное сообщение
"Heartbeat-уязвимость в OpenSSL могла эксплуатироваться с ноя..." Отправлено vn971, 11-Апр-14 23:03
Ээээ, я просто объяснял что значит компьютерно-верифицированная программа.. И, кстати, как и в математике -- доказательства легко можно модифицировать в случае небольших изменений требований в задаче. То есть, версия никуда гвоздями не прибита. Модифицируешь код, модифицируешь доказательство кода -- всё ок. На счёт времени верифицирования -- вы не правы, оно очень мало. Все возможные состояния никто не рассматривает, так же как не рассматривают все возможные состояния неупорядоченного массива когда доказывают корректность bubble sort (мелом на доске).