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

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

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

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

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

教授生平

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

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

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

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

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

他在2015年當(dāng)選CMU名譽(yù)教授。

教計算機(jī)自己檢查錯誤的人走了

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

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

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

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

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

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

責(zé)任編輯：lq