当地时间12月23日，2007年图灵奖得主Edmund M． Clarke（爱德蒙·克拉克）因感染新冠肺炎不幸去世，享年75岁。
当地时间12月23日，2007年图灵奖得主Edmund M． Clarke（爱德蒙·克拉克）因感染新冠肺炎不幸去世，享年75岁。
其子James S． Clarke随后发推文缅怀父亲：“他对我的学术研究有着极高的期望，同时又教我打棒球、钓鱼，以及环游世界。我将深深地铭记他。”
在父亲的影响下，James在学业上也取得了卓越的成就，于1999年获得哈佛大学物理化学博士学位，目前任职英特尔量子硬件研究组总监。
Edmund M． Clarke曾任美国卡内基梅隆大学计算机科学系教授，是ACM和IEEE会士。他在软硬件验证、自动定理证明、形式方法等方面享有崇高的国际声誉，是模型检验方法的开创者之一。
Edmund生平回顾
Edmund出生于1945年，1967年从弗吉尼亚大学获得数学学士学位，1968年从杜克大学获得数学硕士学位，1976年从弗吉尼亚大学获得计算机博士学位。
博士毕业后，Edmund先是在杜克大学任教两年。随后，1978年，他加入哈佛大学担任助理教授。1982年，Clarke离开哈佛，加入卡内基梅隆大学计算机系，并在1989年被评为全职终身教授。
Edmund一直专注于软硬件系统的验证和自动理论证明方面的研究工作。
早在他的博士论文中，便证明了：
某些编程语言控制结构没有良好的Hoare式证明系统。
1981年，他与门下的博士生Allen Emerson首次提出模型检测（model checking）的观点，并将其用在自动及并发系统的验证研究上。他们使用SAT验证完成模型检测，主要针对有界模型。
然而，从理论推导到实际工程应用仍有一定差距，因为实际系统大多是混合系统，而且直接使用数值方法会出现许多错误。为此，Edmund与团队成员开发了dReal实用工具，利用DPLL、间隔算法、限制性算法等思想研究实际问题。
2007年，Edmund M.Clarke与Allen Emerson和Joseph Sifakis共同获得图灵奖，获奖理由是他们开发了模型检测技术，并使之成为一个广泛应用在硬件和软件工业中非常有效的算法验证技术。
正因为Edmund在该领域中的杰出贡献，他还斩获了ACM Paris Kanellakis奖、赫布兰奖、美国国家工程院院士等荣誉和头衔。
Edmund还是中国科学院“爱因斯坦讲席教授”，在2013年10月在中国科学院进行过访问交流。
2013年，Edmund还参加了清华大学的“巅峰对话”活动，席间介绍了自己的学术历程与主要学术成果。他提到，本科期间的学习为他后来的研究打下了坚实的数学基础。他从自己感兴趣的推理和可计算实数出发，着手于实数的非线性问题研究。
对于如何保持积极的科研心态，Edmund表示：自己对于喜欢的事物有一种着魔般的热情，喜欢拼尽全力解决问题；在时间安排上，他会给科研工作留出充足的时间，避免自己过度陷入繁琐的行政工作中。
对于如何培养学生，Edmund强调了两个词：充分的自由与适时的引导。他会给自己的学生一个自由的研究环境，在此基础上加以适度的引导，并着力培养他们专注于探索问题的品质。
至于如何看待数学基础训练的意义，Edmund认为：计算本身就是一件令人兴奋的事情，而数学是学好计算机科学的关键，学习数学的各种算法本质上就是培养一种思维方式，因此，本科生学习数学是很好的。
人类的损失
对于爱德蒙·克拉克的离世，卡内基梅隆大学校长Farnam Jahanian表示，“随着爱德蒙·克拉克的去世，世界失去了一位计算机科学界的巨人，卡内基梅隆大学也告别了一位受人爱戴的成员”。他说，目前学术界才刚刚开始看到爱德蒙在模型检验方面的开创性工作所带来的广泛且长期的益处，他的见解在未来几年还会继续激励研究人员和从业者。
中国科学院大学教授包云岗表示：享年75岁，人类的损失！
网友们在表达哀悼的同时，也给予了Edmund高度的认可：
如果没有他的贡献，很难想象我的领域会是什么样子。
他对科学的贡献是无法估量的。
当 Clarke 去世的消息传来，曾经的学生、威斯康辛大学麦迪逊分校教授 Somesh Jha 在推特上说：「感觉 2020 年不会更糟糕了。」
责编：Yvonne Geng
本文综合自AI科技评论、量子位、澎湃新闻
您可能感兴趣
