作者 | 陳彩嫻、陳大鑫
AI科技評論最新消息，當地時間12月23日，2007年圖靈獎得主Edmund M. Clarke（愛德蒙·克拉克）因感染新冠肺炎不幸去世。
其子James S. Clarke隨後發推文緬懷父親：「他對我的學術研究有著極高的期望，同時又教我打棒球、釣魚，以及環遊世界。我將深深地銘記他。」
在父親的影響下，James在學業上也取得了卓越的成就，於1999年獲得哈佛大學物理化學博士學位，目前任職英特爾量子硬體研究組總監。
Edmund出生於1945年，1967年從維吉尼亞大學獲得數學學士學位，1968年從杜克大學獲得數學碩士學位，1976年從維吉尼亞大學獲得計算機博士學位。
博士畢業後，Edmund先是在杜克大學任教兩年。隨後，1978年，他加入哈佛大學擔任助理教授。1982年，Clarke離開哈佛，加入卡內基梅隆大學計算機系，並在1989年被評為全職終身教授。
Edmund一直專注於軟硬體系統的驗證和自動理論證明方面的研究工作。在他的博士論文中，有一項工作就是證明在一些程序語言的控制邏輯中沒有一個完善的Hoare理論證明系統。
1981年，他與門下的博士生Allen Emerson首次提出模型檢測（model checking）的觀點，並將其用在自動及並發系統的驗證研究上。他們使用SAT驗證完成模型檢測，主要針對有界模型。
然而，從理論推導到實際工程應用仍有一定差距，因為實際系統大多是混合系統，而且直接使用數值方法會出現許多錯誤。為此，Edmund與團隊成員開發了dReal實用工具，利用DPLL、間隔算法、限制性算法等思想研究實際問題。
2007年，Edmund與E Allen Emerson、Joseph Sifakis等兩位科學家一同獲得圖靈獎，獲獎理由是他們開發了模型檢測技術，並使之成為廣泛應用於硬體和軟體工業里的有效算法驗證技術。
2013年，Edmund曾參加了清華大學的「巔峰對話」活動，席間介紹了自己的學術歷程與主要學術成果。他提到，本科期間的學習為他後來的研究打下了堅實的數學基礎。他從自己感興趣的推理和可計算實數出發，著手於實數的非線性問題研究。
對於如何保持積極的科研心態，Edmund表示：自己對於喜歡的事物有一種著魔般的熱情，喜歡拼盡全力解決問題；在時間安排上，他會給科研工作留出充足的時間，避免自己過度陷入繁瑣的行政工作中。
對於如何培養學生，Edmund強調了兩個詞：充分的自由與適時的引導。他會給自己的學生一個自由的研究環境，在此基礎上加以適度的引導，並著力培養他們專注於探索問題的品質。
至於如何看待數學基礎訓練的意義，Edmund認為：計算本身就是一件令人興奮的事情，而數學是學好計算機科學的關鍵，學習數學的各種算法本質上就是培養一種思維方式，因此，本科生學習數學是很好的。
參考連結：
https://news.tsinghua.edu.cn/info/1010/58633.htm
http://m.gerenjianli.com/Mingren/03/o31ttbnps44logs.html
https://en.wikipedia.org/wiki/Edmund_M._Clarke