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

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

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

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

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

生平回顧

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

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

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

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

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

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

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

他免去了陸奇「45 美元的申請手續(xù)費」

對于陸奇來說，Clarke 是「伯樂」一般的存在。

[[359820]]

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

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

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

當 Clarke 去世的消息傳來，曾經(jīng)的學生、威斯康辛大學麥迪遜分校教授 Somesh Jha 在推特上說：「感覺 2020 年不會更糟糕了?！?/p>