當地時間12月23日，英特爾實驗室量子硬體研究組總監James S. Clarke在社交媒體發文表示，他的父親、2007年圖靈獎得主愛德蒙·克拉克（Edmund M. Clarke）因感染新冠肺炎不幸去世。
James S. Clarke在社交媒體發文。愛德蒙·克拉克曾任美國卡內基梅隆大學計算機科學系教授，是ACM和IEEE會士。他在軟硬體驗證、自動定理證明、形式方法等方面享有崇高的國際聲譽，是模型檢驗方法的開創者之一。2007年，Edmund M.Clarke與E Allen Emerson和Joseph Sifakis共同獲得圖靈獎，獲獎理由是他們開發了模型檢測技術，並使之成為一個廣泛應用在硬體和軟體工業中非常有效的算法驗證技術。
對於愛德蒙·克拉克的離世，卡內基梅隆大學校長Farnam Jahanian表示，「隨著愛德蒙·克拉克的去世，世界失去了一位計算機科學界的巨人，卡內基梅隆大學也告別了一位受人愛戴的成員」。他說，目前學術界才剛剛開始看到愛德蒙在模型檢驗方面的開創性工作所帶來的廣泛且長期的益處，他的見解在未來幾年還會繼續激勵研究人員和從業者。
愛德蒙·克拉克出生於1945年，1967年在維吉尼亞大學獲得數學學士學位，1968年在杜克大學獲得數學碩士學位，1976年在康奈爾大學獲得計算機博士學位。然後，克拉克教授在杜克大學任教兩年，於1978年加入哈佛大學並擔任助理教授。1982年，加入卡內基梅隆大學計算機系。
2013年4月，愛德蒙·克拉克在受邀出席清華大學「巔峰對話」活動時介紹過自己的學術歷程和主要學術成果。
據清華大學新聞網報導，出於對計算機的酷愛，博士研究期間愛德蒙·克拉克從數學專業轉到計算機專業。本科期間的學習為後來的研究打下了堅實的數學基礎，從自己感興趣的領域——推理和可計算實數出發，他首先著手於實數的非線性問題。
1981年，愛德蒙·克拉克與自己的博士生首次提出模型檢測的想法，並用在自動機並發系統的驗證研究上，主要使用SAT驗證完成模型檢測，主要針對於有界模型。然而從理論推導到實際工程應用是有距離的，因為實際系統大多都是混合系統，尤其是數值方法直接的使用會出現許多錯誤。為此，愛德蒙教授的團隊針對他們的思想開發出了dReal實用工具，該工具主要利用DPLL、間隔算法、限制性算法等思想研究實際問題。實際中，信息物理系統是一個龐大的系統，對於系統安全性問題的研究至關重要。針對這一研究目標，愛德蒙團隊驗證了卡普了猜想，無人駕駛汽車，心臟模擬仿真等問題。
愛德蒙·克拉克曾獲IEEE Harry M. Goode紀念獎（2004年），Herbrand獎（2008年）。2005年當選美國工程院院士，2011年當選美國藝術和科學院院士。
(本文來自澎湃新聞，更多原創資訊請下載「澎湃新聞」APP)