【導讀】2007年圖靈獎得主愛德蒙·克拉克（Edmund M. Clarke）因感染新冠肺炎于當?shù)貢r間12月22日不幸去世。

當?shù)貢r間12月22日，2007年圖靈獎得主愛德蒙·克拉克（Edmund M. Clarke）因感染新冠肺炎不幸去世，享年75歲。

他的兒子James Clarke在推特上發(fā)布了這一消息。在推文中，James Clarke說：「今天，我的父親愛德蒙·M·克拉克因為新冠肺炎去世了。他是2007年圖靈獎獲得者。父親對我的學術(shù)研究一直寄予厚望，他還教我打棒球，釣魚，環(huán)球旅行。我將會深切懷念他。」

據(jù)了解，James Clarke目前擔任英特爾量子硬件研究組總監(jiān)。

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

教授生平

愛德蒙·克拉克生于1945年，1967年從弗吉尼亞大學獲得數(shù)學學士學位。1976年，康奈爾大學計算機系獲得其博士學位。

1982年，克拉克教授加入卡內(nèi)基梅隆大學計算機科學系；在此之前，他先后在杜克大學和哈佛大學任教，在那里，他的研究小組繼續(xù)開創(chuàng)形式驗證和自動定理證明。

他是計算機輔助驗證會議的創(chuàng)始人之一，也曾擔任過Formal Methods in Systems Design雜志的主編。

1995年，克拉克成為第一個獲得FORE Systems教授資格的人，2008年，他升任大學教授，這也是CMU教師的最高榮譽。

他曾獲得1998年的ACM Kanellakis獎，1999年Allen Newell 研究卓越獎，2004年 IEEE Harry h. Goode 紀念獎以及2008年自動推理演繹會議Herbrand杰出貢獻獎（共同獲得者）。2014年，富蘭克林學會授予他鮑爾科學成就獎，以表彰他在計算機系統(tǒng)驗證技術(shù)的構(gòu)想和開發(fā)方面的領(lǐng)導作用。

他在2015年當選CMU名譽教授。

教計算機自己檢查錯誤的人走了

自計算機誕生以來，工程師們通過運行模擬以測試性能或手動檢查每行計算機代碼的方法來檢查計算機電路或軟件程序中的邏輯錯誤。但是，隨著計算機芯片上組件的數(shù)量呈幾何級數(shù)增長，軟件和計算機系統(tǒng)同樣也變得更加復雜，這些偶然的「非正式驗證」方法顯然是不夠的。錯誤通常在產(chǎn)品發(fā)布后才被發(fā)現(xiàn)，因為即使是微小的錯誤就整起來也非常昂貴的。

1981年，當時在哈佛擔任助理教授的克拉克與他的研究生E. Allen Emerson以及Grenoble大學的Joseph Sifakis，開發(fā)了一種自動檢測計算機硬件和軟件設(shè)計錯誤的方法，被稱為模型檢測。

模型檢測是一種分析設(shè)計背后邏輯的「形式驗證」，就像數(shù)學家使用證明來確定一個定理是正確的。模型檢測考慮硬件或軟件設(shè)計的每一種可能狀態(tài)，并確定它是否與設(shè)計者的規(guī)范一致，大大避免了偶然錯誤的出現(xiàn)，隨后它被廣泛應(yīng)用，幫助提高復雜計算機芯片、系統(tǒng)和網(wǎng)絡(luò)的可靠性。

克拉克教授和E. Allen Emerson， Joseph Sifakis因此獲得了2007年的圖靈獎。

卡內(nèi)基梅隆大學的校長Farnam Jahanian說：「Ed在模型檢測方面的開創(chuàng)性工作將形式化的計算方法應(yīng)用于最終的挑戰(zhàn): 計算機檢查自己的正確性。隨著系統(tǒng)變得越來越復雜，我們才剛剛開始看到Ed的見解所帶來的廣泛和長期的益處，這將在未來幾年繼續(xù)激勵研究人員和實踐者?！?/p>

新冠帶走了克拉克教授，從此世界又少了一個計算機巨人，但天堂沒有新冠，教授，走好！

責任編輯：lq