Сегодня у нас в универе Byron Cook из MS Research в Кембридже провел весьма занимательный семинар, которым мне захотелось поделиться (заранее предупреждаю, что верификация — это совсем не моя область, поэтому я мог что-то неправильно понять).

Байрон — достаточно известный мужик, ктр довольно долго работал в Windows kernel team, а также в свое время начал проект Z3 (это на сегодняшний день самый мощный SMT-солвер). Сейчас он занимается автоматической верификацией, но не столько классической проблемой доказательства отсутствия багов, сколько доказательством того, что кусок кода завершит выполнение. Разумеется, задача неразрешима в силу неразрешимости задачи останова.

Однако, он утверждает, что за последние лет 7-8 они добились существенного прогресса при помощи хитрой процедуры генерации аргументов заверщаемости (termination arguments) и их проверки существующими верификаторами (в частности, SLAM, который, насколько я понял, MS сейчас активно использует при верификации драйверов). Активно развивается проект TERMINATOR, при помощи которого (опять же, по его словам), они сумели доказать завершаемость + незавершаемость для ряда драйверов. Я к сожалению не запомнил, в какой статье приведена таблица с результатами, но можно найти.

К сожалению, сегодняшних слайдов у меня нет, но достаточно похожую лекцию он читал год назад. Я посмотрел, там многое пересекается.

Может кого-то заинтересует.

PS. Запустил поиск (чтоб не запостить баян) и обнаружил, что в 2006 г. проскакивало объявление

Автор: Programmierer AG
Дата: 14.02.06

о работе над Терминатором

Здравствуйте, kl, Вы писали:

Блин, своими словами описал, а абстракт забыл. Вот он:

Software failures can be sorted into two groups: those that cause the software to do something wrong (e.g. crashing), and those that result in the software not doing something useful (e.g. hanging). In recent years automatic tools have been developed which use mathematical proof techniques to certify that software cannot crash. But, based on Alan Turing's proof of the halting problem's undecidablity, many have considered the dream of automatically proving the absence of hangs to be impossible. While not refuting Turing's original result, recent research now makes this dream a reality. This lecture will describe this recent work and its application to industrial software.