12 月 23 日，英特爾量子硬件研究組總監(jiān) James S. Clarke 發(fā)文表示，他的父親、2007 年圖靈獎(jiǎng)得主 Edmund M. Clarke 因感染新冠不幸去世，享年 75 歲。

Edmund M. Clarke 生前就職于卡內(nèi)基梅隆大學(xué)（CMU），是該校的終身教授。1981 年，他與自己的博士生 Allen Emerson 首次提出了模型檢測(cè)的想法并用在自動(dòng)機(jī)并發(fā)系統(tǒng)的驗(yàn)證研究上，成為形式邏輯研究方面模型檢測(cè)（model checking）的開創(chuàng)者之一。模型檢測(cè)是一種自動(dòng)驗(yàn)證技術(shù)，主要通過顯式狀態(tài)搜索或隱式不動(dòng)點(diǎn)計(jì)算來(lái)驗(yàn)證有窮狀態(tài)并發(fā)系統(tǒng)的模態(tài) / 命題性質(zhì)。

由于模型檢測(cè)可以自動(dòng)執(zhí)行，并能在系統(tǒng)不滿足性質(zhì)時(shí)提供反例路徑，因此在工業(yè)界比演繹證明更受推崇。盡管限制在有窮系統(tǒng)上是一個(gè)缺點(diǎn)，但模型檢測(cè)可以應(yīng)用于許多非常重要的系統(tǒng)，如硬件控制器和通信協(xié)議等有窮狀態(tài)系統(tǒng)。很多情況下，可以把模型檢測(cè)和各種抽象與歸納原則結(jié)合起來(lái)驗(yàn)證非有窮狀態(tài)系統(tǒng)（如實(shí)時(shí)系統(tǒng)）。

作為這一領(lǐng)域的先驅(qū)，Clarke 不僅開創(chuàng)了模型檢測(cè)技術(shù)，還使之成為一個(gè)廣泛應(yīng)用在硬件和軟件工業(yè)中非常有效的算法驗(yàn)證技術(shù)，并因此獲得 2007 年的圖靈獎(jiǎng)。

對(duì)于 Clarke 的不幸離世，CMU 校長(zhǎng) Farnam Jahanian 表示了沉痛悼念：「Ed Clarke 離開了，這個(gè)世界又失去了一位計(jì)算機(jī)科學(xué)領(lǐng)域的巨人，此時(shí) CMU 要向這位我們深愛的成員告別。Ed 在模型檢測(cè)方面的開拓性工作將形式化的計(jì)算方法應(yīng)用于終極挑戰(zhàn)：讓計(jì)算機(jī)檢查自身的正確性。隨著系統(tǒng)變得越來(lái)越復(fù)雜，我們才剛剛認(rèn)識(shí)到 Ed 的洞察所帶來(lái)的廣泛而深遠(yuǎn)的益處，這將在未來(lái)數(shù)年持續(xù)激勵(lì)研究人員和從業(yè)人員前行。」

生平回顧

和很多計(jì)算機(jī)領(lǐng)域的大牛一樣，Edmund Clarke 本科階段學(xué)的并不是計(jì)算機(jī)，而是更為基礎(chǔ)性的學(xué)科——數(shù)學(xué)。由于熱愛計(jì)算機(jī)，他博士階段選擇了康奈爾大學(xué)的計(jì)算機(jī)專業(yè)，并于 1976 年拿到博士學(xué)位。

本科期間的學(xué)習(xí)為 Edmund Clarke 后來(lái)的研究打下了堅(jiān)實(shí)的數(shù)學(xué)基礎(chǔ)。他從自己感興趣的領(lǐng)域——推理和可計(jì)算實(shí)數(shù)出發(fā)，首先著手于實(shí)數(shù)的非線性問題。1981 年，他與自己的博士生首次提出模型檢測(cè)的想法，并用在自動(dòng)機(jī)并發(fā)系統(tǒng)的驗(yàn)證研究上，主要使用 SAT 驗(yàn)證完成模型檢測(cè)，針對(duì)有界模型。

然而從理論推導(dǎo)到實(shí)際工程應(yīng)用是有距離的，因?yàn)閷?shí)際系統(tǒng)大多都是混合系統(tǒng)，尤其是數(shù)值方法直接的使用會(huì)出現(xiàn)許多錯(cuò)誤。為此，Edmund Clarke 的團(tuán)隊(duì)針對(duì)他們的思想開發(fā)出了 dReal 實(shí)用工具，該工具主要利用 DPLL、間隔算法、限制性算法等思想研究實(shí)際問題。實(shí)際中，信息物理系統(tǒng)是一個(gè)龐大的系統(tǒng)，對(duì)于系統(tǒng)安全性問題的研究至關(guān)重要。針對(duì)這一研究目標(biāo)，Edmund Clarke 團(tuán)隊(duì)驗(yàn)證了無(wú)人駕駛汽車、心臟模擬仿真等問題。

在加入 CMU 計(jì)算機(jī)系之前，Edmund Clarke 曾在杜克大學(xué)和哈佛大學(xué)任教，還是計(jì)算機(jī)輔助驗(yàn)證會(huì)議的創(chuàng)始人之一，以及《系統(tǒng)設(shè)計(jì)形式方法》雜志的前主編。1989 年，Edmund Clarke 被評(píng)為 CMU 全職終身教授。

1995 年，Clarke 成為第一位獲得 FORE Systems 教授職位的人，并于 2008 年被任命為 University Professor，這是 CMU 的最高教師榮譽(yù)。他是 1998 年 ACM Kanellakis 獎(jiǎng)、1999 年 Allen Newell 杰出研究獎(jiǎng)、2004 年 IEEE Harry H. Goode 紀(jì)念獎(jiǎng)和自動(dòng)證明會(huì)議 2008 年 Herbrand 獎(jiǎng)自動(dòng)推理杰出貢獻(xiàn)獎(jiǎng)的獲獎(jiǎng)?wù)摺?014 年，富蘭克林研究所向 Clarke 頒發(fā)了鮑爾科學(xué)成就獎(jiǎng)，以表彰他在計(jì)算機(jī)系統(tǒng)驗(yàn)證技術(shù)的概念和開發(fā)方面的引領(lǐng)作用。

曾和 Clarke 在 CMU 共事的計(jì)算機(jī)科學(xué)家 Randal E. Bryant 這樣介紹他：「Ed Clarke 是一位杰出的研究者，同時(shí)是一個(gè)善良、充滿愛心的人。我非常欽佩他指導(dǎo)博士生和博士后研究人員的能力，其中許多人通過自己的學(xué)術(shù)研究影響了全世界。」

除了培養(yǎng)人才方面的杰出能力，Clarke 在發(fā)現(xiàn)人才方面也是慧眼獨(dú)具，前百度副總裁、現(xiàn)奇績(jī)創(chuàng)壇創(chuàng)始人兼 CEO 陸奇便是他發(fā)現(xiàn)的人才之一。

他免去了陸奇「45 美元的申請(qǐng)手續(xù)費(fèi)」

對(duì)于陸奇來(lái)說(shuō)，Clarke 是「伯樂」一般的存在。

[[359820]]

上世紀(jì) 80 年代末，陸奇剛剛在復(fù)旦大學(xué)計(jì)算機(jī)系讀完本科和研究生，并留校任教。Edmund Clarke 受邀來(lái)到復(fù)旦講課，對(duì)陸奇在其研討會(huì)上提出的問題產(chǎn)生了深刻印象。

會(huì)后，Edmund Clarke 看了陸奇的論文，隨后邀請(qǐng)他申請(qǐng) CMU 的博士項(xiàng)目。得知在大學(xué)任教的陸奇月薪僅有幾十元人民幣，Clarke 免去了 45 美元的申請(qǐng)手續(xù)費(fèi)并提供了獎(jiǎng)學(xué)金。1996 年，陸奇獲得了卡內(nèi)基梅隆大學(xué)的計(jì)算機(jī)博士學(xué)位。

退休以后，Clarke 一直住在匹茲堡的養(yǎng)老院。盡管已經(jīng)患上老年癡呆癥，但他仍然能夠回憶起自己的第一臺(tái)計(jì)算機(jī)。

當(dāng) Clarke 去世的消息傳來(lái)，曾經(jīng)的學(xué)生、威斯康辛大學(xué)麥迪遜分校教授 Somesh Jha 在推特上說(shuō)：「感覺 2020 年不會(huì)更糟糕了。」