Здравствуйте, K.V.R, Вы писали:

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

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

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

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

Начните с классики: Э.Дейкстра "Дисциплина программирования" и Д.Грис "Наука программирования". Все есть в открытом доступе на http://www.oberon2005.ru/ilog.html