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

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

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

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

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

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

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

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