Премия Тьюринга была вручена Эдмунду М. Кларку (Edmund M. Clarke) в 2007 году за его новаторскую разработку проверки моделей — метода формальной верификации аппаратного и программного обеспечения. Его работа установила строгие математические методы обеспечения корректности сложных электронных систем, фундаментально изменив подход инженеров к надежности современной вычислительной инфраструктуры на протяжении его долгой академической карьеры.
Академическое становление
Кларк родился в Ньюпорт-Ньюсе в 1945 году и прошел традиционный путь через математику, прежде чем перейти в информатику. Он получил степень бакалавра математики в Университете Вирджинии в 1967 году, а затем степень магистра в Университете Дьюка в 1968 году. Свое формальное образование он завершил в 1976 году, получив докторскую степень по компьютерным наукам в Корнеллском университете, где его диссертационная работа продемонстрировала критические ограничения существующих систем доказательств в стиле Хоара для структур управления языков программирования.
Карьерный рост
Кларк занимал должности в нескольких крупных учреждениях, прежде чем обосноваться в Университете Карнеги — Меллона. После получения докторской степени он два года преподавал в Университете Дьюка, а затем в 1978 году перешел в Гарвардский университет на должность доцента. В 1982 году он присоединился к факультету компьютерных наук в Карнеги — Меллоне. К 1989 году он получил полное профессорское звание и в 1995 году был назначен первым профессором FORE Systems. К 2015 году он перешел в статус почетного профессора.
Вклад в формальную верификацию
В 1981 году Кларк и его студент Э. Аллен Эмерсон (E. Allen Emerson) представили проверку моделей — метод верификации конечных параллельных систем. Его исследовательская группа впоследствии стала пионером в методах верификации оборудования и символьной проверки моделей с использованием бинарных диаграмм решений. Помимо этих основных усилий, его команда разработала параллельный доказыватель теорем Parthenon и систему символьных вычислений Analytica. В 2009 году он основал центр вычислительного моделирования и анализа сложных систем для применения этих методов к биологическим и встроенным системам.
Двадцать вопросов, восемь минут на часах и процентиль, измеренный по всем, кто его проходил. Без регистрации.
Пройти тест IQ →Профессиональное признание
Исследования Кларка получили многочисленные награды, включая премию Пэриса Канеллакиса в 1998 году, мемориальную премию Гарри Х. Гуда в 2004 году и премию Эрбрана в 2008 году. В 2005 году он был избран членом Национальной инженерной академии, а в 2011 году — членом Американской академии искусств и наук. В 2014 году он получил премию Бауэра и премию за достижения в науке от Института Франклина за свое лидерство в автоматизированной верификации систем.
Краткие факты
- Рождение: 1945, Ньюпорт-Ньюс - Смерть: 2020, Питтсбург - Образование: Университет Вирджинии (1967), Университет Дьюка (1968), Корнеллский университет (1976) - Основная область: Компьютерные науки - Главное признание: Премия Тьюринга ACM 2007 - Членство: ACM, IEEE, Национальная инженерная академия - Академический дом: Университет Карнеги — Меллона
Вопросы читателей
### Что такое проверка моделей?
Это метод формальной верификации, разработанный Кларком и Э. Алленом Эмерсоном для обеспечения корректности аппаратного и программного обеспечения.
### Занимал ли Кларк именную кафедру?
Да, он был первым обладателем кафедры FORE Systems в Университете Карнеги — Меллона, начиная с 1995 года.
