Jump to content

Эдмунд М. Кларк

(Перенаправлено от Эдмунда Кларка )
Эдмунд М. Кларк
Рожденный
Эдмунд Мелсон Кларк-младший

( 1945-07-27 ) 27 июля 1945 г.
Умер 22 декабря 2020 г. ) ( 2020-12-22 ) ( 75 лет
Альма-матер Корнелльский университет
Известный Проверка модели
Награды Премия AM Тьюринга
Научная карьера
Поля Информатика
Учреждения Университет Карнеги-Меллон
Диссертация Теоремы о полноте и неполноте для систем аксиом типа Хоара   (1976)
Докторантура Роберт Ли Констебль
Докторанты
Веб-сайт www .cs .cmu .edu /~emc

Эдмунд Мелсон Кларк-младший (27 июля 1945 — 22 декабря 2020) — американский учёный-компьютерщик и учёный, известный разработкой проверки моделей — метода формальной проверки аппаратного и программного обеспечения . Он был FORE Systems профессором компьютерных наук в Университете Карнеги-Меллон . Кларк вместе с Э. Алленом Эмерсоном и Джозефом Сифакисом получил в 2007 году от ACM премию Тьюринга .

Биография

[ редактировать ]

Кларк родился в Ньюпорт-Ньюсе, штат Вирджиния , и получил бакалавра степень математики в Университете Вирджинии , Шарлоттсвилл , в 1967 году, магистра степень математики в Университете Дьюка , Дарем, Северная Каролина , в 1968 году, а также степень доктора философии. Получил степень в области компьютерных наук в Корнеллском университете , Итака, штат Нью-Йорк, в 1976 году. После получения докторской степени он в течение двух лет преподавал на факультете компьютерных наук в Университете Дьюка . В 1978 году он переехал в Гарвардский университет , Кембридж, Массачусетс , где работал доцентом кафедры компьютерных наук на факультете прикладных наук . Он покинул Гарвард в 1982 году, чтобы поступить на факультет компьютерных наук Университета Карнеги-Меллон , Питтсбург, Пенсильвания . В 1989 году он был назначен профессором. В 1995 году он стал первым лауреатом звания профессора систем FORE , заведующего кафедрой в Школе компьютерных наук Карнеги-Меллона . Он стал профессором университета в 2008 году и стал почетным профессором в 2015 году. [ 2 ]

Он умер от COVID-19 в декабре 2020 года в возрасте 75 лет во время пандемии COVID-19 в Пенсильвании . [ 3 ] [ 4 ]

В круг интересов Кларка входили программного и аппаратного обеспечения проверка и автоматическое доказательство теорем . В своей докторской диссертации В своей диссертации он доказал, что некоторые структуры управления языками программирования не имеют хороших систем доказательств в стиле Хоара . В 1981 году он и его доктор философии. Студент Э. Аллен Эмерсон первым предложил использовать проверку моделей в качестве метода проверки для параллельных систем с конечным состоянием . Его исследовательская группа стала пионером в использовании проверки моделей для проверки аппаратного обеспечения . символьную проверку модели с использованием бинарных диаграмм решений Его группа также разработала . Эта важная техника была предметом докторской диссертации Кеннета Макмиллана. диссертация, получившая ACM награду за докторскую диссертацию . Кроме того, его исследовательская группа разработала первое с параллельным разрешением средство доказательства теорем (Parthenon) и средство доказательства теорем, основанное на системе символьных вычислений (Analytica). [ 5 ] . В 2009 году он возглавил создание центра вычислительного моделирования и анализа сложных систем (CMACS), финансируемого Национальным научным фондом . В этом центре работает команда исследователей из нескольких университетов, применяющих абстрактную интерпретацию и проверку моделей к биологическим и встроенным системам .

Профессиональное признание

[ редактировать ]

был членом ACM Кларк и IEEE . Он получил Премию за техническое совершенство от Корпорации исследований полупроводников в 1995 году и Премию Аллена Ньюэлла за выдающиеся достижения в исследованиях от Карнеги-Меллона факультета компьютерных наук в 1999 году. Он был одним из лауреатов премии вместе с Рэндалом Брайантом , Э. Алленом Эмерсоном и Кеннетом. Макмиллану премии ACM Paris Kanellakis в 1999 году за разработку символической проверки моделей . В 2004 году он получил от компьютерного общества IEEE Мемориальную премию Гарри Х. Гуда за значительный и новаторский вклад в формальную верификацию аппаратных и программных систем, а также за глубокое влияние, которое этот вклад оказал на электронную промышленность. Он был избран членом Национальной инженерной академии в 2005 году за вклад в формальную проверку правильности аппаратного и программного обеспечения. Он был избран членом Американской академии искусств и наук в 2011 году. В 2008 году он получил премию Эрбрана в «признании его роли в изобретении проверки моделей и его устойчивого лидерства в этой области на протяжении более двух десятилетий». В 2012 году он получил почетную докторскую степень Венского технического университета за выдающийся вклад в область информатики. В 2014 году он получил премию Бауэра и премию за достижения в области науки от Института Франклина за «ведущую роль в концепции и разработке методов автоматической проверки правильности широкого спектра компьютерных систем, в том числе используемых в транспорте, связи и лекарство." Он был членом Sigma Xi и Phi Beta Kappa .

См. также

[ редактировать ]
  1. ^ Эдмунд Мелсон Кларк-младший.
  2. ^ «Эдмунд М. Кларк» . Cs.cmu.edu . Проверено 24 декабря 2020 г.
  3. ^ Джеймс С. Кларк [@Jim_in_Oregon] (22 декабря 2020 г.). «Мой отец, Эдмунд М. Кларк, скончался сегодня от Covid. [...]» ( Твит ) – через Твиттер .
  4. ^ «Эдмунд Кларк — новаторский метод обнаружения ошибок программного обеспечения и оборудования | Школа компьютерных наук Карнеги-Меллона» . Cs.cmu.edu . Проверено 24 декабря 2020 г.
  5. ^ Бауэр, Андрей; Кларк, Эдмунд; Чжао, Сюдун (1998). «Аналитика - эксперимент по сочетанию доказательства теорем и символьных вычислений». Журнал автоматизированного рассуждения . 21 (3): 295–325. дои : 10.1023/А:1006079212546 .
[ редактировать ]
Arc.Ask3.Ru: конец переведенного документа.
Arc.Ask3.Ru
Номер скриншота №: 5018f511aca234fad2a5b0105a4073bc__1723032420
URL1:https://arc.ask3.ru/arc/aa/50/bc/5018f511aca234fad2a5b0105a4073bc.html
Заголовок, (Title) документа по адресу, URL1:
Edmund M. Clarke - Wikipedia
Данный printscreen веб страницы (снимок веб страницы, скриншот веб страницы), визуально-программная копия документа расположенного по адресу URL1 и сохраненная в файл, имеет: квалифицированную, усовершенствованную (подтверждены: метки времени, валидность сертификата), открепленную ЭЦП (приложена к данному файлу), что может быть использовано для подтверждения содержания и факта существования документа в этот момент времени. Права на данный скриншот принадлежат администрации Ask3.ru, использование в качестве доказательства только с письменного разрешения правообладателя скриншота. Администрация Ask3.ru не несет ответственности за информацию размещенную на данном скриншоте. Права на прочие зарегистрированные элементы любого права, изображенные на снимках принадлежат их владельцам. Качество перевода предоставляется как есть. Любые претензии, иски не могут быть предъявлены. Если вы не согласны с любым пунктом перечисленным выше, вы не можете использовать данный сайт и информация размещенную на нем (сайте/странице), немедленно покиньте данный сайт. В случае нарушения любого пункта перечисленного выше, штраф 55! (Пятьдесят пять факториал, Денежную единицу (имеющую самостоятельную стоимость) можете выбрать самостоятельно, выплаичвается товарами в течение 7 дней с момента нарушения.)