愛德蒙·克拉克

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

基本介紹

• 外文名：Edmund Clarke
• 國籍：美國
• 出生日期：1945年7月27日
• 職業：教授
• 畢業院校：維吉尼亞大學，杜克大學，康奈爾大學
• 主要成就：開發出模型檢測技術
  圖靈獎(2007)

研究工作

他的工作之一就是證明的在一些程式語言的控制邏輯中沒有一個完善的Hoare理論證明系統。

個人成就

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

個人榮譽

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