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

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

他的兒子James Clarke在推特上發(fā)布了這一消息。在推文中，James Clarke說：「今天，我的父親愛德蒙·M·克拉克因?yàn)樾鹿诜窝兹ナ懒?。他?007年圖靈獎(jiǎng)獲得者。父親對我的學(xué)術(shù)研究一直寄予厚望，他還教我打棒球，釣魚，環(huán)球旅行。我將會深切懷念他?！?/p>

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

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

教授生平

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

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

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

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

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

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

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

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

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

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

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

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

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

責(zé)任編輯：lq