Посоветуйте рессурсы по автоматической верификации программ, в первую очередь интересуют научные труды в этой области, статьи, диссертации и т.д., во вторую — готовые инструменты и методики.

Прежде всего хотелось бы понять постановку задачи, т.е. узнать ответ на вопрос "что надо верифицировать в программах и что _можно_ верифицировать в программах? (безопасность/непритиворечивость|конечность алгоритмов/что-то еще)"
Во вторых интересно как находятся ответы на вопросы постевленные выше (существующие теоретические [и практические] разработки)
В третьих — выяснить какова достоверность существующих теорий и их программных воплощений. Проще говоря насколько можно доверять инструментым типа valgrind, purify, lint, spin и т.д.

Есть ли в России разработки в области автоматической верификации?

Если у кого-то есть опыт применения верифицирующих методик, подходов и инструментов в реальной жизни — поделитесь опытом применения.