愛德蒙·克拉克 - 簡介

愛德蒙·克拉克（Edmund Clarke）(born July 27, 1945)，1967年Clarke從美國南部的弗吉尼亞大學獲得了其數(shù)學的學士學位，然后1968年從杜克大學完成了其數(shù)學的碩士學位的學業(yè)。9年之后的1976年，從康奈爾大學計算機系獲得其博士學位。然后，Clarke在杜克大學任教兩年。1978年，加入了哈佛大學并擔任助理教授一職。1982年，Clarke離開哈佛加入了卡內基梅隆大學計算機系，并在1989年被評為全職終身教授一職。

愛德蒙·克拉克 - 研究工作

Clarke一直專注于軟硬件系統(tǒng)的驗證和自動理論證明方面的研究工作。在他的博士論文中，其工作之一就是證明的在一些程序語言的控制邏輯中沒有一個完善的Hoare理論證明系統(tǒng)。

愛德蒙·克拉克 - 成就

1981年，他與自己的博士生Allen Emerson首次提出了模型檢查的想法并用在自動機并發(fā)系統(tǒng)的驗證研究上。成為形式邏輯研究方面模型檢查的開創(chuàng)者之一。

愛德蒙·克拉克 - 獲獎

2007年度圖靈獎授予Edmund M. Clarke、E Allen Emerson和Joseph Sifakis三位科學家，表彰他們開發(fā)模型檢測技術，并使之成為一個廣泛應用在硬件和軟件工業(yè)中非常有效的算法驗證技術所做的奠基性貢獻。

愛德蒙·克拉克 - 相關資料

圖靈獎由美國計算機協(xié)會于1966年設立，專門獎勵那些對計算機事業(yè)做出重要貢獻的個人，其名稱取自計算機科學先驅，英國科學家阿蘭?圖靈。獲獎者的貢獻必須在計算機領域具有持久而重大的影響。

圖靈獎有“計算機界諾貝爾獎”之稱，對獲獎者要求極高，評獎程序亦極嚴格，目前由英特爾和Google公司贊助，獎金為25萬美元。

目前獲此殊榮的華人科學家僅姚期智一人。