Тьюринговская премия, выдаваемая Association for Computing Machinery, самым крупным в мире компьютерным научно-образовательным сообществом, основанным в 1947 году, была учреждена в 1966 году. Премия вручается за вклад в усовершенствование компьютерных технологий. Чтобы ее получить, нужно сделать нечто такое, что имеет значимость для практического развития компьютерных систем. Это объясняет и состав награжденных ею, и то, почему академические работы не могут быть основанием для номинации. (Тем, кто сетует на отсутствие среди награжденных этой премией наших соотечественников, следует учитывать необходимость наличия практического применения у награждаемых работ.)
Невзирая на высокий статус, Тьюринговская премия скорее почетна, чем финансово значима. И если сравнивать ее с призовыми награждениями теннисистов или гонорарами в кино и шоу-бизнесе, то ее денежное выражение ничтожно. Пока единственным спонсором премии была корпорация Intel, размер премии составлял всего 100 тыс. долл. С подключением Google он вырос до 250 тыс. Традиционно премию называют «Нобелевской премией в компьютерных науках», хотя это явное преувеличение: и уровень почета, и масштаб вознаграждения явно не в пользу Тьюринговской премии.
Лауреатами 2007 года стали Эдмунд Кларк (Университет Карнеги-Меллона), Аллен Эммерсон (Техасский университет в Остине) и Джозеф Сифаркис (Гренобльский университет, Франция). Они награждены за достижения в области, называемой в оригинале model checking, а по-русски — «верификацией моделей». Перевод оставляет впечатление, что проверка моделей является целью, однако это всего лишь средство. Если быть точным, то model checking — скорее не верификация самой модели, а метод проверки какой-либо системы с использованием модели. Верификация с использованием модели — один из четырех теоретически возможных способов проверки проекта аппаратных или программных систем; помимо него выделяют еще имитационное моделирование, тестирование и дедуктивную верификацию.
Методы model checking позволяют алгоритмически верифицировать формальные системы. Они в большей степени подходят к аппаратным системам, чем к программным, поскольку последние не всегда удается описать формально. Поэтому область применения model checking пока ограничена моделированием аппаратуры и в лучшем случае аппаратно-программных встроенных систем. Базисом для model checking служит математический аппарат темпоральной логики (temporal logic), то есть такой логики, в которой присутствует фактор времени. Эта разновидность логики была предложена в 60-е годы, обычно ее появление связывают с именами Амира Пнуели и Зохара Манна. Лауреаты премии Тьюринга смогли приложить аппарат темпоральной логики к решению практических задач, создав методы формальной верификации систем. Признанным родоначальником model checking является профессор Университета Карнеги-Меллона Эдмунд Кларк. Его книга, ставшая классической (Э.М. Кларк, О. Грамберг, Д. Пелед «Верификация моделей программ: Model Checking»), переведена на русский язык. Еще две школы model checking сложились в университетах Остина и Гренобля, ими руководили соответственно профессора Аллен Эммерсон и Джозеф Сифаркис.
По оценкам специалистов, у model checking большое будущее, которое связано с крупными программными системами.