冬至剛過，許多人在這一天燒紙錢祭奠先祖。過去的一年，無論是否新冠疫情的關係，國內國外各行各業都走了不少我們熟悉的面孔。
例如，80後看著長大的春晚第一代主持人，趙忠祥老師。
亦或是傳奇賭王何鴻燊
喜歡看NBA的同學自然忘不了，那個永遠的24號、永遠的黑曼巴，科比
漫威世界也告別了「黑豹」查德維克博斯曼
而前幾天，讓計算機圈子格外惋惜的是，當地時間12月22日，2007年圖靈獎得主，美國著名計算機專家，愛德蒙·克拉克（Edmund M. Clarke）因感染新冠肺炎不幸去世，享年75歲。
在他去世的第二天，他的兒子，也是英特爾實驗室量子硬體研究組的總監，James S. Clarke在社交媒體上公布了這個信息
或許，圈外人對這個名字陌生的外國老者並不是很熟悉。
愛德蒙·克拉克，1982年，作為教授加入卡耐基梅隆大學計算機科學系；在那之前，他曾在杜克大學和哈佛大學任教，並獲得過杜克大學的數學碩士學位及康奈爾大學的計算機博士學位，在1989年被評為全職終身教授一職。
他是計算機輔助驗證會議的創始人之一，也是ACM和IEEE會士，同時曾擔任過Formal Methods in Systems Design雜誌的主編。他在軟硬體驗證、自動定理證明、形式方法等方面享有崇高的國際聲譽，是模型檢測方法的開創者之一。
2007年，克拉克教授與艾倫·愛默生教授（Allen Emerson）和約瑟夫·斯發基斯（Joseph Sifakis）共同獲得有著計算科學領域諾貝爾之稱的圖靈獎。獲獎理由是他們開發的模型檢測技術，成為一個廣泛應用在硬體和軟體工業中非常有效的算法驗證技術。
自計算機誕生以來，工程師們通過模擬運行來測試性能，並通過手動檢查每一行代碼來檢測計算機電路或軟體程序中的邏輯錯誤。但隨著計算機軟體和系統日益複雜化，這些「非正式驗證」的方法顯然無法很好地解決問題。而克拉克教授等人開發的模型檢測技術，可以有效的分析設計背後的邏輯，就像數學家用證明來確定一個定理是正確的一樣。模型檢測能夠考慮到硬體和軟體設計的每種可能狀態，並確定它是否與設計規範相一致。可以說，克拉克教授他們的發明，極大的減少了在產品發布後才發現錯誤造成的昂貴代價，推動了整個計算機行業的發展。
對於克拉克教授的離世，卡耐基梅隆大學校長Farnam Jahanian表示，「隨著愛德蒙·克拉克的去世，世界失去了一位計算機科學界的巨人，卡耐基梅隆大學也告別了一位受人愛戴的成員」。卡耐基梅隆大學計算機科學學院院長Martial Hebert也表示，「治學嚴謹是愛德蒙·克拉克的一大特點，這為他贏得了計算機科學界的最高榮譽，也貫穿了他30多年的計算機科學生涯。」
同時，克拉克教授還是一位和中國頗有緣分的大師，他曾於2013年4月受邀出席清華大學「巔峰對話」，並在活動中介紹自己的學術歷程和主要學術成果。當時他表示，正是出於對計算機的酷愛，博士研究期間他從數學專業轉到計算機專業。不知道有多少清華學子在那次活動後義無反顧的改學了計算機。而前微軟全球執行副總裁陸奇，在復旦大學取得碩士學位後，選擇留校任教，正是在一次克拉克教授的演講中與其相識，最終赴卡耐基梅隆大學就讀，並於1996年5月畢業，獲得了計算機科學博士學位。
克拉克教授還曾獲得過ACM Kanellakis獎（1998年），Allen Newell卓越研究獎（1999年）、IEEE Harry H. Goode紀念獎（2004年），Herbrand獎（2008年）。1995年成為第一個擁有FORE Systems教授資格的人，2005年當選美國工程院院士，2008年升任卡耐基梅隆大學教師最高榮譽University Professor，2011年當選美國藝術和科學院院士。2014年，富蘭克林學會向他頒發了鮑爾科學成就獎，表彰他在計算機系統驗證技術的構思和開發方面的領導作用。
新冠就這樣帶走了一位計算機界的巨人，或許就是因為上帝在有人和他打籃球之後，又想有人教他用下計算機吧，教授一路走好!
掃一掃，關注我
知曉前沿科技，領略技術魅力