新智元 發表於 2021-01-14 10:36:07
【導讀】2007年圖靈獎得主愛德蒙·克拉克（Edmund M. Clarke）因感染新冠肺炎於當地時間12月22日不幸去世。
當地時間12月22日，2007年圖靈獎得主愛德蒙·克拉克（Edmund M. Clarke）因感染新冠肺炎不幸去世，享年75歲。
他的兒子James Clarke在推特上發布了這一消息。在推文中，James Clarke說：「今天，我的父親愛德蒙·M·克拉克因為新冠肺炎去世了。他是2007年圖靈獎獲得者。父親對我的學術研究一直寄予厚望，他還教我打棒球，釣魚，環球旅行。我將會深切懷念他。」
據了解，James Clarke目前擔任英特爾量子硬體研究組總監。
克拉克教授生前一直專注於軟硬體系統的驗證和自動理論證明方面的研究工作。在他的博士論文中，有一項工作就是證明在一些程序語言的控制邏輯中沒有一個完善的Hoare理論證明系統。
教授生平
愛德蒙·克拉克生於1945年，1967年從維吉尼亞大學獲得數學學士學位。1976年，康奈爾大學計算機系獲得其博士學位。
1982年，克拉克教授加入卡內基梅隆大學計算機科學系；在此之前，他先後在杜克大學和哈佛大學任教，在那裡，他的研究小組繼續開創形式驗證和自動定理證明。
他是計算機輔助驗證會議的創始人之一，也曾擔任過Formal Methods in Systems Design雜誌的主編。
1995年，克拉克成為第一個獲得FORE Systems教授資格的人，2008年，他升任大學教授，這也是CMU教師的最高榮譽。
他曾獲得1998年的ACM Kanellakis獎，1999年Allen Newell 研究卓越獎，2004年 IEEE Harry h. Goode 紀念獎以及2008年自動推理演繹會議Herbrand傑出貢獻獎（共同獲得者）。2014年，富蘭克林學會授予他鮑爾科學成就獎，以表彰他在計算機系統驗證技術的構想和開發方面的領導作用。
他在2015年當選CMU名譽教授。
教計算機自己檢查錯誤的人走了
自計算機誕生以來，工程師們通過運行模擬以測試性能或手動檢查每行計算機代碼的方法來檢查計算機電路或軟體程序中的邏輯錯誤。但是，隨著計算機晶片上組件的數量呈幾何級數增長，軟體和計算機系統同樣也變得更加複雜，這些偶然的「非正式驗證」方法顯然是不夠的。錯誤通常在產品發布後才被發現，因為即使是微小的錯誤就整起來也非常昂貴的。
1981年，當時在哈佛擔任助理教授的克拉克與他的研究生E. Allen Emerson以及Grenoble大學的Joseph Sifakis，開發了一種自動檢測計算機硬體和軟體設計錯誤的方法，被稱為模型檢測。
模型檢測是一種分析設計背後邏輯的「形式驗證」，就像數學家使用證明來確定一個定理是正確的。模型檢測考慮硬體或軟體設計的每一種可能狀態，並確定它是否與設計者的規範一致，大大避免了偶然錯誤的出現，隨後它被廣泛應用，幫助提高複雜計算機晶片、系統和網絡的可靠性。
克拉克教授和E. Allen Emerson， Joseph Sifakis因此獲得了2007年的圖靈獎。
卡內基梅隆大學的校長Farnam Jahanian說：「Ed在模型檢測方面的開創性工作將形式化的計算方法應用於最終的挑戰: 計算機檢查自己的正確性。隨著系統變得越來越複雜，我們才剛剛開始看到Ed的見解所帶來的廣泛和長期的益處，這將在未來幾年繼續激勵研究人員和實踐者。」
新冠帶走了克拉克教授，從此世界又少了一個計算機巨人，但天堂沒有新冠，教授，走好！
責任編輯：lq
打開APP閱讀更多精彩內容
聲明：本文內容及配圖由入駐作者撰寫或者入駐合作網站授權轉載。文章觀點僅代表作者本人，不代表電子發燒友網立場。文章及其配圖僅供工程師學習之用，如有內容圖片侵權或者其他問題，請聯繫本站作侵刪。 侵權投訴