Эдмунд Мелсон Кларк-младший (27 июля 1945 г. — 22 декабря 2020 г.) — американский учёный-компьютерщик и учёный, известный разработкой проверки моделей , метода формальной проверки проектов оборудования и программного обеспечения . Он был профессором компьютерных наук в Университете Карнеги — Меллона . Кларк вместе с Э. Алленом Эмерсоном и Джозефом Сифакисом получил премию ACM Turing Award 2007 года .
Родился в Ньюпорт-Ньюс, Вирджиния , Кларк получил степень бакалавра по математике в Университете Вирджинии , Шарлоттсвилл , в 1967 году, степень магистра по математике в Университете Дьюка , Дарем, Северная Каролина , в 1968 году и степень доктора философии по компьютерным наукам в Корнеллском университете , Итака, Нью-Йорк, в 1976 году. После получения степени доктора философии он преподавал на кафедре компьютерных наук в Университете Дьюка в течение двух лет. В 1978 году он перешел в Гарвардский университет , Кембридж, Массачусетс , где был доцентом компьютерных наук в Отделении прикладных наук . Он покинул Гарвард в 1982 году, чтобы присоединиться к факультету компьютерных наук в Университете Карнеги-Меллона , Питтсбург, Пенсильвания . Он был назначен полным профессором в 1989 году. В 1995 году он стал первым получателем профессорской должности FORE Systems , почетной кафедры в Школе компьютерных наук Карнеги-Меллона . В 2008 году он стал профессором университета, а в 2015 году — почетным профессором. [2]
Он умер от COVID-19 в декабре 2020 года в возрасте 75 лет во время пандемии COVID-19 в Пенсильвании . [3] [4]
Интересы Кларка включали проверку программного и аппаратного обеспечения и автоматическое доказательство теорем . В своей докторской диссертации он доказал, что некоторые структуры управления языком программирования не имеют хороших систем доказательств в стиле Хоара . В 1981 году он и его аспирант Э. Аллен Эмерсон впервые предложили использовать проверку моделей в качестве метода проверки для конечных параллельных систем . Его исследовательская группа стала пионером в использовании проверки моделей для проверки оборудования . Символическая проверка моделей с использованием диаграмм бинарных решений также была разработана его группой. Этот важный метод был предметом докторской диссертации Кеннета Макмиллана, которая получила премию ACM Doctoral Dissertation Award. Кроме того, его исследовательская группа разработала первую систему доказательства теорем с параллельным разрешением (Parthenon) и систему доказательства теорем, основанную на системе символических вычислений (Analytica). [5] В 2009 году он руководил созданием центра вычислительного моделирования и анализа сложных систем (CMACS), финансируемого Национальным научным фондом . В этом центре работает группа исследователей из нескольких университетов, которые применяют абстрактную интерпретацию и проверку моделей к биологическим и встроенным системам .
Кларк был членом ACM и IEEE . Он получил премию Technical Excellence Award от Semiconductor Research Corporation в 1995 году и премию Allen Newell Award за выдающиеся достижения в исследованиях от Carnegie Mellon Computer Science Department в 1999 году. Он был одним из победителей вместе с Randal Bryant , E. Allen Emerson и Kenneth McMillan премии ACM Paris Kanellakis Award в 1999 году за разработку символической проверки моделей . В 2004 году он получил премию IEEE Computer Society Harry H. Goode Memorial Award за значительный и новаторский вклад в формальную верификацию аппаратных и программных систем и за глубокое влияние, которое эти вклады оказали на электронную промышленность. Он был избран в Национальную инженерную академию в 2005 году за вклад в формальную верификацию корректности аппаратных и программных средств. Он был избран в Американскую академию искусств и наук в 2011 году. Он получил премию Herbrand Award в 2008 году в «признание его роли в изобретении проверки моделей и его постоянного лидерства в этой области на протяжении более двух десятилетий». В 2012 году он получил почетную докторскую степень от TU Wien за выдающийся вклад в область информатики. Он получил премию Bower Award и премию за достижения в науке 2014 года от Института Франклина за «его ведущую роль в разработке концепции и разработке методов автоматической проверки правильности широкого спектра компьютерных систем, включая те, которые используются в транспорте, связи и медицине». Он был членом Sigma Xi и Phi Beta Kappa .
