巨星陨落！2007年图灵奖得主Edmund Clarke因感染新冠离世...-技术圈

冬至刚过，许多人在这一天烧纸钱祭奠先祖。过去的一年，无论是否新冠疫情的关系，国内国外各行各业都走了不少我们熟悉的面孔。

例如，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年，富兰克林学会向他颁发了鲍尔科学成就奖，表彰他在计算机系统验证技术的构思和开发方面的领导作用。

新冠就这样带走了一位计算机界的巨人，或许就是因为上帝在有人和他打篮球之后，又想有人教他用下计算机吧，教授一路走好!