История изменений
Исправление XVilka, (текущая версия) :
Знаю я про формальную верификацию, SMT-солверы, z3 от Microsoft и т.д. Но! Формализация программы - это одно, верификация - другое. Саму программу на Си, почти невозможно формально верифицировать. Для этого пишут их на Ocaml, Haskell или других подобных языках. А потом надо будет переводить в Си/Си++. Вот на этапе перевода могут и вылезти ошибки, и никакая верификация не поможет.
Да, при работе с реальным железом никакой верификации быть не может. Достаточно небольшого бага в железе, например в том же USB или сетевом контроллере, и можно этим воспользоваться.
Исходная версия XVilka, :
Знаю я про формальную верификацию, SMT-солверы, z3 от Microsoft и т.д. Но! Формализация программы - это одно, верификация - другое. Саму программу на Си, почти невозможно формально верифицировать. Для этого пишут их на Ocaml, Haskell или других подобных языках. А потом надо будет переводить в Си/Си++. Вот на этапе перевода могут и вылезти ошибки, и никакая верификация не поможет.