Эдмунд М. Кларк - Edmund M. Clarke
 | Эта статья включает в себя список общих Рекомендации, но он остается в основном непроверенным, потому что ему не хватает соответствующих встроенные цитаты. (Февраль 2013) (Узнайте, как и когда удалить этот шаблон сообщения) |
Эдмунд Мелсон Кларк-младший | |
|---|---|
 | |
| Родившийся | 27 июля 1945 г. |
| Национальность | Американец |
| Альма-матер | Корнелл Университет |
| Известен | Проверка модели |
| Награды | ЯВЛЯЮСЬ. Премия Тьюринга |
| Научная карьера | |
| Поля | Информатика |
| Учреждения | Университет Карнеги Меллон |
| Тезис | Теоремы о полноте и неполноте для систем аксиом типа Хоара (1976) |
| Докторант | Роберт Ли Констебль |
| Докторанты | |
| Интернет сайт | www |
Эдмунд Мелсон Кларк-младший (родился 27 июля 1945 г.), американец на пенсии. специалист в области информатики и академический отмечен для развитияпроверка модели, метод формальной проверки конструкции аппаратного и программного обеспечения. FORE Systems Профессор Информатика Почетный в Университет Карнеги Меллон. Кларк вместе с Э. Аллен Эмерсон и Джозеф Сифакис, является лауреатом 2007 г. Ассоциация вычислительной техники ЯВЛЯЮСЬ. Премия Тьюринга.
биография
Кларк получил Б.А. степень в области математика от Университет Вирджинии, Шарлоттсвилль, Вирджиния, в 1967 г. М.А. степень в области математика из Университет Дьюка, Дарем, Северная Каролина, в 1968 г. и Кандидат наук. степень в области Информатика из Корнелл Университет, Итака, штат Нью-Йорк в 1976 г. После получения докторской степени преподавал на факультете компьютерных наук в Университет Дьюка, два года. В 1978 году переехал в Гарвардский университет, Кембридж, Массачусетс где он был доцентом Информатика в Отдел прикладных наук. Он покинул Гарвард в 1982 году, чтобы поступить на факультет компьютерных наук в Университет Карнеги Меллон, Питтсбург, Пенсильвания. Он был назначен профессором в 1989 году. В 1995 году он стал первым лауреатом FORE Systems Профессорство, кафедра в Школа компьютерных наук Карнеги-Меллона. Он стал профессором университета в 2008 году и стал почетным профессором в 2015 году.[1]
Работа
Интересы Кларка включают программного обеспечения и аппаратное обеспечение проверка и автоматическое доказательство теорем. В его докторской степени. диссертации он доказал, что определенные язык программирования управляющие структуры не имели хороших Системы доказательства Хоара. В 1981 году он и его докторская степень. ученик Э. Аллен Эмерсон впервые предложил использовать проверка модели как метод проверки для Конечные параллельные системы. Его исследовательская группа была пионером в использовании проверка модели за проверка оборудования. Символический проверка модели с помощью диаграммы бинарных решений также был разработан его группой. Этот важный метод был предметом доктора философии Кеннета Макмиллана. дипломная работа, получившая ACM Докторская Диссертация Премия. Кроме того, его исследовательская группа разработала первое параллельное разрешение средство доказательства теорем (Парфенон) и первое средство доказательства теорем, основанное на системе символьных вычислений (Analytica). В 2009 году он возглавил создание Центра вычислительного моделирования и анализа сложных систем (CMACS), финансируемого Национальный фонд науки. В этом центре работает команда исследователей из нескольких университетов, абстрактная интерпретация и проверка модели к биологическим и встроенным системам.
Профессиональное признание
Кларк - это парень из ACM и IEEE. Он получил награду за техническое совершенство от Корпорация полупроводниковых исследований в 1995 году и Аллен Ньюэлл Награда за выдающиеся достижения в области исследований от Университет Карнеги-Меллона Информатика Кафедры в 1999 году. Был со-победителем вместе с Рэндал Брайант, Э. Аллен Эмерсон, и Кеннет Макмиллан из ACM Премия Пэрис Канеллакис в 1999 году для разработки проверка символьной модели. В 2004 году получил IEEE Computer Society Гарри Х. Гуд Премия Мемориала за значительный и новаторский вклад в формальную проверку аппаратных и программных систем, а также за огромное влияние, которое этот вклад оказал на электронную промышленность. Он был избран в Национальная инженерная академия в 2005 г. за вклад в формальную проверку правильности аппаратного и программного обеспечения. Он был избран в Американская академия искусств и наук в 2011 году. Он получил Премия Herbrand в 2008 году в «признании его роли в изобретении проверки моделей и его устойчивого лидерства в этой области более двух десятилетий». Он получил 2014 Премия Бауэра и премия за достижения в науке от Институт Франклина за «его ведущую роль в концепции и разработке методов автоматической проверки правильности широкого спектра компьютерных систем, включая те, которые используются в транспорте, связи и медицине». Он является членом Сигма Си и Пхи Бета Каппа.
