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

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

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

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

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

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

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

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

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

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

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

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

Под автоматической верификацией Вы понимаете то что делает, например lint ?

KVR>Прежде всего хотелось бы понять постановку задачи, т.е. узнать ответ на вопрос "что надо верифицировать в программах и что _можно_ верифицировать в программах? (безопасность/непритиворечивость|конечность алгоритмов/что-то еще)"

Например, есть некоторая функция. Есть как минимум два варианта проверить ее корректность: проверить корректность результатов при всех возможных аргументах, или _доказать_ что функция всегда выдает корректный результат. Первый вариант напоминает unittesting, и не всегда может гарантировать "правильность" функции (особенно когда область допустимых значений бесконечна). Доказательство корректности оправдано применять в случае сложных и "тяжелых" алгоритмов. Хороший пример — оптимизирующий компилятор : необходимо гарантировать что оптимизированный код выполняет то же что и исходный(+ не хуже по некоторым характеристикам). Такие доказательства проводят в рамках некоторой формализованной системы. Одной из таких является ACL2. На этой же странице есть ссылки на "some industrial-scale examples".

Статьи по теме есть здесь