Войти
| Эдмунд Мелсон Кларк-младший | |
|---|---|
 | |
| Родился | (1945-07-27) 27 июля, 1945 |
| Национальность | Американец |
| Alma mater | Корнельский университет |
| Известен | Проверка моделей |
| Награды | AM Премия Тьюринга |
| Научная карьера | |
| Области | Информатика |
| Учреждения | Университет Карнеги-Меллона |
| Диссертация | Теоремы о полноте и неполноте для систем аксиом типа Хоара (1976) |
| Докторская советник | Роберт Ли Констебл |
| Докторанты | |
| Веб-сайт | www.cs.cmu.edu / ~ emc |
Эдмунд Мелсон Кларк, Младший (родился 27 июля 1945 г.) - американский пенсионер компьютерный ученый и академик, известный разработкой проверки моделей, метода формальной проверки оборудования. и разработка программного обеспечения. Он FORE Systems профессор компьютерных наук заслуженный в Университете Карнеги-Меллона. Кларк вместе с Э. Аллен Эмерсон и Джозеф Сифакис, является получателем 2007 Association for Computing Machinery A.M. Премия Тьюринга.
Кларк получил степень BA по математике в Университете Вирджинии, Шарлоттсвилль, Вирджиния, в 1967 году, MA степень по математике от Университета Дьюка, Дарем, Северная Каролина, в 1968 году и докторская степень по компьютерам Science из Корнельского университета, Итака, штат Нью-Йорк, в 1976 году. После получения докторской степени он преподавал на факультете компьютерных наук в Университете Дьюка, два года. В 1978 году он переехал в Гарвардский университет, Кембридж, Массачусетс, где он был доцентом компьютерных наук в Отделении прикладных наук.. Он покинул Гарвард в 1982 году, чтобы работать на факультете компьютерных наук в Университете Карнеги-Меллона, Питтсбург, Пенсильвания. Он был назначен профессором в 1989 году. В 1995 году он стал первым обладателем звания FORE Systems Professorship, кафедрой Школы компьютерных наук Карнеги-Меллона. Он стал профессором университета в 2008 году и стал почетным профессором в 2015 году.
Интересы Кларка включают программное обеспечение и аппаратное обеспечение верификацию и автоматическое доказательство теорем. В его докторской степени. В своей диссертации он доказал, что некоторые управляющие структуры языка программирования не имеют хороших систем доказательства в стиле Хоара. В 1981 году он и его докторская степень. студент Э. Аллен Эмерсон первым предложил использовать проверку модели в качестве метода проверки для параллельных систем с конечным числом состояний. Его исследовательская группа была пионером в использовании проверки моделей для проверки оборудования. Символьная проверка модели с использованием диаграмм двоичных решений также была разработана его группой. Этот важный метод был предметом доктора философии Кеннета Макмиллана. дипломная работа, получившая премию ACM Докторская Диссертация. Кроме того, его исследовательская группа разработала первое средство доказательства теорем с параллельной разрешающей способностью (Парфенон) и первое средство доказательства теорем, основанное на системе символьных вычислений (Analytica). В 2009 году он возглавил создание Центра вычислительного моделирования и анализа сложных систем (CMACS), финансируемого Национальным научным фондом. В этом центре работает группа исследователей из нескольких университетов, применяющих абстрактную интерпретацию и проверку моделей для биологических и встроенных систем.
Кларк является членом ACM и IEEE. В 1995 г. он получил награду за техническое совершенство от Semiconductor Research Corporation и награду Аллена Ньюэлла за выдающиеся достижения в исследованиях от Carnegie Mellon Computer Science Департамент в 1999 году. Он был одним из победителей вместе с Рэндалом Брайантом, Э. Аллен Эмерсон и обладатель премии ACM Paris Kanellakis Award в 1999 году за разработку проверки символьных моделей. В 2004 году он получил награду IEEE Computer Society Harry H. Goode Memorial Award за значительный и новаторский вклад в формальную проверку аппаратных и программных систем, а также за глубокое влияние, которое этот вклад оказал на электронная промышленность. Он был избран членом Национальной инженерной академии в 2005 году за вклад в формальную проверку правильности аппаратного и программного обеспечения. Он был избран членом Американской академии искусств и наук в 2011 году. Он получил премию Хербранда в 2008 году «в знак признания его роли в изобретении проверки моделей и его устойчивого лидерства в области уже более двух десятилетий ". Он получил в 2014 году премию Бауэра и премию за достижения в науке от Института Франклина за «свою ведущую роль в концепции и разработке методов автоматической проверки правильности широкого спектра компьютерные системы, в том числе используемые в транспорте, связи и медицине ». Он является членом Sigma Xi и Phi Beta Kappa.
 | Wikimedia У Commons есть СМИ, связанные с Эдмундом М. Кларком. |
