Исследовательская лаборатория Microsoft при Кэмриджском универсистете разрабатывает проект TERMINATOR. Основной целью проекта является создание методов и программных средств автоматического доказательства того факта, что промышленный программный компонент не может зависнуть.
В 1936 году Алан Тьюринг, считающийся отцом-сонователем современной вычислительной математики и в честь которого Ассоциация Вычислительной Техники (ACM) назвала одну из престижнейший наград в области вычислительной математики (премия Алана Тьюринга), доказал, что не существует общего алгоритма проверки для возможных программ и всех возможных входных данных завершится ли их выполнение как было задумано или нет (часто эту проблему кратко именуют "проблемой останова").
По прошествии 70 лет, Байрон Кук (Byron Cook), исследователь из Microsoft, при поддержке своих европейских коллег подготовил ряд лекций, описывающих новые методы автоматического доказательства завершения программ в большинстве практических случаев. Со слов самого Кука, доказательство Тьюринга вовсе не противоречит тому, что однажды будут созданы методы решения проблемы останова, работающие в 99.9% случаев на программах, написаных человеком. Именно на создание таких методов и направлена работа Байрона Кука и его коллег.
Проект TERMINATOR является практическим применение этих методов. Его первая версия (v0.1), поддерживающая вложенные циклы, рекурсивные функции, указатели, побочные эффекты и т.д., была успешно применена к драйверам Windows размером до 35000 строк исходного кода.
//Microsoft Research