人物生平
1967年在弗吉尼亞大學(xué)獲得數(shù)學(xué)學(xué)士學(xué)位,1968年在杜克大學(xué)獲得數(shù)學(xué)碩士學(xué)位,1976年在康奈爾大學(xué)獲得計算機(jī)博士學(xué)位。然后,克拉克教授在杜克大學(xué)任教兩年,于1978年加入哈佛大學(xué)并擔(dān)任助理教授。1982年,加入卡內(nèi)基梅隆大學(xué)計算機(jī)系。
研究工作
他的工作之一就是證明的在一些程序語言的控制邏輯中沒有一個完善的Hoare理論證明系統(tǒng)。
個人成就
1981年,他與自己的博士生Allen Emerson首次提出了模型檢測的想法并用在自動機(jī)并發(fā)系統(tǒng)的驗證研究上。成為形式邏輯研究方面模型檢查的開創(chuàng)者之一。
個人榮譽(yù)
2007年度圖靈獎授予Edmund M. Clarke、E Allen Emerson和Joseph Sifakis三位科學(xué)家,表彰他們開發(fā)模型檢測技術(shù),并使之成為一個廣泛應(yīng)用在硬件和軟件工業(yè)中非常有效的算法驗證技術(shù)所做的奠基性貢獻(xiàn)。
曾獲IEEE Harry M. Goode紀(jì)念獎(2004年),Herbrand獎(2008年)。2005年當(dāng)選美國工程院院士,2011年當(dāng)選美國藝術(shù)和科學(xué)院院士。
人物逝世
2020年12月23日,因感染新冠肺炎不幸去世。