 | Эта статья включает в себя список общих ссылок , но он остается в значительной степени непроверенным, поскольку в нем отсутствует достаточное количество соответствующих встроенных ссылок . ( Февраль 2013 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения ) |
Эдмунд М. Кларк | |
|---|---|
 | |
| Родившийся | Эдмунд Мелсон Кларк-младший 27 июля 1945 г. Ньюпорт-Ньюс, Вирджиния , США |
| Умер | 22 декабря 2020 г. (75 лет) |
| Национальность | Американец |
| Альма-матер | Корнелл Университет |
| Известен | Проверка модели |
| Награды | Премия AM Тьюринга |
| Научная карьера | |
| Поля | Информатика |
| Учреждения | Университет Карнеги Меллон |
| Тезис | Теоремы о полноте и неполноте для систем аксиом типа Хоара (1976) |
| Докторант | Роберт Ли Констебль |
| Докторанты | |
| Интернет сайт | www |
Эдмунд Мелсон Кларк-младший (27 июля 1945 - 22 декабря 2020) был американским компьютерным ученым и академиком, известным разработкой проверки моделей - метода формальной проверки конструкции аппаратного и программного обеспечения. Он был почетным профессором компьютерных наук FORE Systems в Университете Карнеги-Меллона . Кларк, наряду с Э. Аллен Эмерсон и Джозеф Sifakis , был получателем 2007 Ассоциация по вычислительной технике А.М. Премия Тьюринга .
Биография [ править ]
Кларк получил бакалавра степень в области математики из Университета Вирджинии , Charlottesville, VA , в 1967 г. в М. степень в области математики из университета Duke , Durham NC , в 1968 году, и Ph.D. степень в области компьютерных наук из Корнельского университета , Итака Нью - Йорк в 1976 г. Получив степень доктора философии, он преподавал на факультете компьютерных наук в Университете Дьюка , в течение двух лет. В 1978 году он переехал в Гарвардский университет , Кембридж, Массачусетс.где он был доцентом компьютерных наук в отделе прикладных наук . Он покинул Гарвард в 1982 году, чтобы работать на факультете компьютерных наук в Университете Карнеги-Меллона , Питтсбург, Пенсильвания . Он был назначен профессором в 1989 году. В 1995 году он стал первым обладателем звания профессора систем FORE , кафедры компьютерных наук Карнеги-Меллона . Он стал профессором университета в 2008 году и стал почетным профессором в 2015 году. [2] Он умер от COVID-19 во время пандемии COVID-19 в Пенсильвании в 2020 году. [3] [4]
Работа [ править ]
Интересы Кларка включали программную и аппаратную верификацию и автоматическое доказательство теорем . В его докторской степени. В своей диссертации он доказал, что определенные структуры управления в языке программирования не имеют хороших систем доказательства в стиле Хоара . В 1981 году он и его докторская степень. Студент Э. Аллен Эмерсон впервые предложил использовать проверку моделей в качестве метода проверки для параллельных систем с конечным числом состояний . Его исследовательская группа впервые применила проверку моделей для проверки оборудования . Проверка символьной модели с использованием бинарных диаграмм решенийтакже был разработан его группой. Этот важный метод был предметом доктора философии Кеннета Макмиллана. тезис, который получил ACM Докторантура Диссертационный Award. Кроме того, его исследовательская группа разработала первое средство доказательства теорем с параллельным разрешением (Парфенон) и первое средство доказательства теорем, основанное на системе символьных вычислений (Analytica). В 2009 году он возглавил создание Центра вычислительного моделирования и анализа сложных систем (CMACS), финансируемого Национальным научным фондом . В этом центре работает команда исследователей из нескольких университетов, применяющих абстрактную интерпретацию и проверку моделей для биологических и встроенных систем.
Профессиональное признание [ править ]
Кларк был парень из АКМ и IEEE . Он получил Премию технического мастерства от Semiconductor Research Corporation в 1995 году и Премию Аллена Ньюэлла за выдающиеся достижения в исследованиях от Департамента компьютерных наук Карнеги-Меллона в 1999 году. Он был одним из победителей вместе с Рэндалом Брайантом , Э. Алленом Эмерсоном и Кеннетом. Макмиллану премии ACM Paris Kanellakis в 1999 году за разработку символической проверки моделей . В 2004 году он получил награду IEEE Computer Society Harry H. Goode. Премия Мемориала за значительный и новаторский вклад в формальную проверку аппаратных и программных систем, а также за глубокое влияние, которое этот вклад оказал на электронную промышленность. Он был избран членом Национальной инженерной академии в 2005 году за вклад в формальную проверку правильности аппаратного и программного обеспечения. В 2011 году он был избран членом Американской академии искусств и наук . В 2008 году он получил премию Herbrand Award как «признание его роли в изобретении модельных проверок и его устойчивого лидерства в этой области на протяжении более двух десятилетий». Он получил премию Бауэра 2014 года и приз за достижения в науке от Института Франклина.за «его ведущую роль в концепции и разработке методов автоматической проверки правильности широкого спектра компьютерных систем, включая те, которые используются в транспорте, связи и медицине». Он был членом Sigma Xi и Phi Beta Kappa .
См. Также [ править ]
- Список пионеров информатики
Ссылки [ править ]
- ↑ Эдмунд Мелсон Кларк-младший.
- ^ "Эдмунд М. Кларк" . Cs.cmu.edu . Проверено 24 декабря 2020 года .
- ^ Джеймс С. Кларк [@Jim_in_Oregon] (22 декабря 2020 г.). «Мой отец, Эдмунд М. Кларк, скончался сегодня от Ковида. [...]» (твит) - через Twitter .
- ^ "Эдмунд Кларк впервые разработал методы обнаружения программных и аппаратных ошибок | Школа компьютерных наук Карнеги-Меллона" . Cs.cmu.edu . Проверено 24 декабря 2020 года .
Внешние ссылки [ править ]
 | Викискладе есть медиафайлы по теме Эдмунда Кларка . |
- Эдмунд М. Кларк на проекте « Математическая генеалогия»
- Домашняя страница Университета Карнеги-Меллона
- Биография онлайн с домашней страницы
- Объявление премии Тьюринга
- Модель Контрольная книга
- Домашняя страница CMACS
- Список публикаций от Microsoft Academic
