模型檢測先驅Edmund Clarke因新冠逝世

機器之心報導

作者：蛋醬、張倩

2020 還能更糟糕嗎？

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

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

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

作為這一領域的先驅，Clarke 不僅開創了模型檢測技術，還使之成為一個廣泛應用在硬體和軟體工業中非常有效的算法驗證技術，並因此獲得 2007 年的圖靈獎。

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

生平回顧

和很多計算機領域的大牛一樣，Edmund Clarke 本科階段學的並不是計算機，而是更為基礎性的學科——數學。由於熱愛計算機，他博士階段選擇了康奈爾大學的計算機專業，並於 1976 年拿到博士學位。

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

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

在加入 CMU 計算機系之前，Edmund Clarke 曾在杜克大學和哈佛大學任教，還是計算機輔助驗證會議的創始人之一，以及《系統設計形式方法》雜誌的前主編。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 獎自動推理傑出貢獻獎的獲獎者。2014 年，富蘭克林研究所向 Clarke 頒發了鮑爾科學成就獎，以表彰他在計算機系統驗證技術的概念和開發方面的引領作用。

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

除了培養人才方面的傑出能力，Clarke 在發現人才方面也是慧眼獨具，前百度副總裁、現奇績創壇創始人兼 CEO 陸奇便是他發現的人才之一。

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

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

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

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

退休以後，Clarke 一直住在匹茲堡的養老院。儘管已經患上老年痴呆症，但他仍然能夠回憶起自己的第一臺計算機。

當 Clarke 去世的消息傳來，曾經的學生、威斯康辛大學麥迪遜分校教授 Somesh Jha 在推特上說：「感覺 2020 年不會更糟糕了。」

參考連結：

https://www.cs.cmu.edu/news/edmund-clarke-pioneered-methods-detecting-software-hardware-errors

https://news.tsinghua.edu.cn/info/1010/58633.htm

https://baike.baidu.com/item/%E6%A8%A1%E5%9E%8B%E6%A3%80%E6%B5%8B/5628442

http://m.gerenjianli.com/Mingren/03/o31ttbnps44logs.html

https://www.cmu.edu/cmtoday/issues/october-2010-issue/feature-stories/bing-it-on/index.html