當地時間12月23日，英特爾實驗室量子硬體研究組總監James S. Clarke在社交媒體發文表示，他的父親、2007年圖靈獎得主愛德蒙·克拉克(Edmund M. Clarke)因感染新冠肺炎不幸去世。
愛德蒙·克拉克曾任美國卡耐基梅隆大學計算機科學系教授，是ACM和IEEE會士。他在軟硬體驗證、自動定理證明、形式方法等方面享有崇高的國際聲譽，是模型檢測方法的開創者之一。對於愛德蒙·克拉克的離世，卡耐基梅隆大學校長Farnam Jahanian表示，「隨著愛德蒙·克拉克的去世，世界失去了一位計算機科學界的巨人，卡耐基梅隆大學也告別了一位受人愛戴的成員」。他說，目前學術界才剛剛開始看到愛德蒙在模型檢測方面的開創性工作所帶來的廣泛且長期的益處，他的見解在未來幾年還會繼續激勵研究人員和從業者。
因開發模型檢測技術獲圖靈獎
愛德蒙·克拉克出生於1945年，1967年在維吉尼亞大學獲得數學學士學位，1968年在杜克大學獲得數學碩士學位，1976年在康奈爾大學獲得計算機博士學位。然後，克拉克教授在杜克大學任教兩年，於1978年加入哈佛大學並擔任助理教授。1982年，加入卡耐基梅隆大學計算機系。
2007年，愛德蒙·克拉克與艾倫·愛默生教授(Allen Emerson)和約瑟夫·斯發基斯(Joseph Sifakis)共同獲得圖靈獎，該獎項有計算機科學領域的「諾貝爾獎」之稱。獲獎理由是他們開發了模型檢測技術，並使之成為一個廣泛應用在硬體和軟體工業中非常有效的算法驗證技術。
自計算機誕生以來，工程師們通過模擬運行來測試性能，並通過手動檢查每一行代碼來檢測計算機電路或軟體程序中的邏輯錯誤。但隨著計算機軟體和系統日益複雜化，這些「非正式驗證」的方法顯然無法很好地解決問題。
相比之下，愛德蒙·克拉克等人開發的模型檢測技術可以分析設計背後的邏輯，就像數學家用證明來確定一個定理是正確的一樣。模型檢測能夠考慮到硬體和軟體設計的每種可能狀態，並確定它是否與設計規範相一致。
1981年，愛德蒙·克拉克與自己的博士生首次提出模型檢測的想法，並用在自動機並發系統的驗證研究上，主要使用SAT驗證完成模型檢測，主要針對於有界模型。然而從理論推導到實際工程應用是有距離的，因為實際系統大多都是混合系統，尤其是數值方法直接的使用會出現許多錯誤。為此，愛德蒙教授的團隊針對他們的思想開發出了dReal實用工具，該工具主要利用DPLL、間隔算法、限制性算法等思想研究實際問題。
晚年仍記得自己的第一臺計算機
卡耐基梅隆大學計算機科學學院院長Martial Hebert表示，治學嚴謹是愛德蒙·克拉克的一大特點，這為他贏得了計算機科學界的最高榮譽，也貫穿了他30多年的計算機科學生涯。
2013年4月，愛德蒙·克拉克在受邀出席清華大學「巔峰對話」活動時介紹過自己的學術歷程和主要學術成果。據清華大學新聞網報導，出於對計算機的酷愛，博士研究期間愛德蒙·克拉克從數學專業轉到計算機專業。本科期間的學習為後來的研究打下了堅實的數學基礎。
在那次演講中，愛德蒙·克拉克強調了數學基礎訓練之於計算機研究的重要性。他說，「計算是一件令人興奮的事情，數學則是做好計算機科學的關鍵，數學的各種算法本質上是培養一種思維方式，這對於本科生無疑是很好的一個專業。」
愛德蒙·克拉克還是前微軟全球執行副總裁陸奇的伯樂。據媒體報導，陸奇1987年在復旦大學取得碩士學位後，選擇留校任教。一次，他去聽愛德蒙·克拉克的演講，在會場上以自己的問題徵服了克拉克邀請他前往卡耐基梅隆大學讀書。後來，陸奇赴卡耐基梅隆大學讀書並於1996年5月畢業，獲得計算機科學博士學位。
2015年，愛德蒙·克拉克成為卡耐基梅隆大學的榮譽退休教授(emeritus professor)。退休以後，克拉克一直住在位於美國匹茲堡的養老院中，並患上了老年痴呆症。他的兒子James S. Clarke曾表示，儘管父親患有晚年老年痴呆症，卻仍能夠回憶起自己的第一臺計算機。
愛德蒙·克拉克曾獲IEEE Harry M. Goode紀念獎(2004年)，Herbrand獎(2008年)。2005年當選美國工程院院士，2011年當選美國藝術和科學院院士。