Автоматизация верификации программ

Верификация программ – метод установления правильности программ при помощи строгих средств.
При этом программа будет считаться правильной, если решит поставленную задачу.
В основе метода верификации лежит предположение о том, что существует некоторая программная документация, соответствие которой нужно доказать.
Верификация программ - трудоемкий процесс, и его целесообразно автоматизировать. Проблемы корректности программы алгоритмически неразрешимы, поэтому не следует рассчитывать на полную автоматизацию.