来源：新智元

当地时间12月22日，2007年图灵奖得主爱德蒙·克拉克（Edmund M. Clarke）因感染新冠肺炎不幸去世，享年75岁。

他的儿子James Clarke在推特上发布了这一消息。在推文中，James Clarke说：「今天，我的父亲爱德蒙·M·克拉克因为新冠肺炎去世了。他是2007年图灵奖获得者。父亲对我的学术研究一直寄予厚望，他还教我打棒球，钓鱼，环球旅行。我将会深切怀念他。」

据了解，JamesClarke目前担任英特尔量子硬件研究组总监。

克拉克教授生前一直专注于软硬件系统的验证和自动理论证明方面的研究工作。在他的博士论文中，有一项工作就是证明在一些程序语言的控制逻辑中没有一个完善的Hoare理论证明系统。

教授生平

爱德蒙·克拉克生于1945年，1967年从弗吉尼亚大学获得数学学士学位。1976年，康奈尔大学计算机系获得其博士学位。

1982年，克拉克教授加入卡内基梅隆大学计算机科学系；在此之前，他先后在杜克大学和哈佛大学任教，在那里，他的研究小组继续开创形式验证和自动定理证明。

他是计算机辅助验证会议的创始人之一，也曾担任过Formal Methods in Systems Design杂志的主编。

1995年，克拉克成为第一个获得FORE Systems教授资格的人，2008年，他升任大学教授，这也是CMU教师的最高荣誉。

他曾获得1998年的ACM Kanellakis奖，1999年Allen Newell 研究卓越奖，2004年 IEEE Harry h. Goode 纪念奖以及2008年自动推理演绎会议Herbrand杰出贡献奖（共同获得者）。2014年，富兰克林学会授予他鲍尔科学成就奖，以表彰他在计算机系统验证技术的构想和开发方面的领导作用。

他在2015年当选CMU名誉教授。

教计算机自己检查错误的人走了

自计算机诞生以来，工程师们通过运行模拟以测试性能或手动检查每行计算机代码的方法来检查计算机电路或软件程序中的逻辑错误。但是，随着计算机芯片上组件的数量呈几何级数增长，软件和计算机系统同样也变得更加复杂，这些偶然的「非正式验证」方法显然是不够的。错误通常在产品发布后才被发现，因为即使是微小的错误就整起来也非常昂贵的。

1981年，当时在哈佛担任助理教授的克拉克与他的研究生E. Allen Emerson以及Grenoble大学的Joseph Sifakis，开发了一种自动检测计算机硬件和软件设计错误的方法，被称为模型检查。

模型检查是一种分析设计背后逻辑的「形式验证」，就像数学家使用证明来确定一个定理是正确的。模型检查考虑硬件或软件设计的每一种可能状态，并确定它是否与设计者的规范一致，大大避免了偶然错误的出现，随后它被广泛应用，帮助提高复杂计算机芯片、系统和网络的可靠性。

克拉克教授和E. Allen Emerson， Joseph Sifakis因此获得了2007年的图灵奖。

卡内基梅隆大学的校长Farnam Jahanian说：「Ed在模型检验方面的开创性工作将形式化的计算方法应用于最终的挑战: 计算机检查自己的正确性。随着系统变得越来越复杂，我们才刚刚开始看到Ed的见解所带来的广泛和长期的益处，这将在未来几年继续激励研究人员和实践者。」

新冠带走了克拉克教授，从此世界又少了一个计算机巨人，但天堂没有新冠，教授，走好！

参考链接：

https://www.cmu.edu/news/stories/archives/2020/december/obituary-ed-clarke.html