哀悼！2007年图灵奖得主Edmund Clarke因感染新冠逝世

作者 | 陈彩娴、陈大鑫

AI科技评论最新消息，当地时间12月23日，2007年图灵奖得主Edmund M. Clarke（爱德蒙·克拉克）因感染新冠肺炎不幸去世。

其子James S. Clarke随后发推文缅怀父亲：“他对我的学术研究有着极高的期望，同时又教我打棒球、钓鱼，以及环游世界。我将深深地铭记他。”

在父亲的影响下，James在学业上也取得了卓越的成就，于1999年获得哈佛大学物理化学博士学位，目前任职英特尔量子硬件研究组总监。

Edmund出生于1945年，1967年从弗吉尼亚大学获得数学学士学位，1968年从杜克大学获得数学硕士学位，1976年从弗吉尼亚大学获得计算机博士学位。

博士毕业后，Edmund先是在杜克大学任教两年。随后，1978年，他加入哈佛大学担任助理教授。1982年，Clarke离开哈佛，加入卡内基梅隆大学计算机系，并在1989年被评为全职终身教授。

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

1981年，他与门下的博士生Allen Emerson首次提出模型检测（model checking）的观点，并将其用在自动及并发系统的验证研究上。他们使用SAT验证完成模型检测，主要针对有界模型。

然而，从理论推导到实际工程应用仍有一定差距，因为实际系统大多是混合系统，而且直接使用数值方法会出现许多错误。为此，Edmund与团队成员开发了dReal实用工具，利用DPLL、间隔算法、限制性算法等思想研究实际问题。

2007年，Edmund与E Allen Emerson、Joseph Sifakis等两位科学家一同获得图灵奖，获奖理由是他们开发了模型检测技术，并使之成为广泛应用于硬件和软件工业里的有效算法验证技术。

2013年，Edmund曾参加了清华大学的“巅峰对话”活动，席间介绍了自己的学术历程与主要学术成果。他提到，本科期间的学习为他后来的研究打下了坚实的数学基础。他从自己感兴趣的推理和可计算实数出发，着手于实数的非线性问题研究。

对于如何保持积极的科研心态，Edmund表示：自己对于喜欢的事物有一种着魔般的热情，喜欢拼尽全力解决问题；在时间安排上，他会给科研工作留出充足的时间，避免自己过度陷入繁琐的行政工作中。

对于如何培养学生，Edmund强调了两个词：充分的自由与适时的引导。他会给自己的学生一个自由的研究环境，在此基础上加以适度的引导，并着力培养他们专注于探索问题的品质。

至于如何看待数学基础训练的意义，Edmund认为：计算本身就是一件令人兴奋的事情，而数学是学好计算机科学的关键，学习数学的各种算法本质上就是培养一种思维方式，因此，本科生学习数学是很好的。

参考链接：

//news.tsinghua.edu.cn/info/1010/58633.htm

//m.gerenjianli.com/Mingren/03/o31ttbnps44logs.html

//en.wikipedia.org/wiki/Edmund_M._Clarke

点击阅读原文，直达AAAI小组！

由于微信公众号试行乱序推送，您可能不再能准时收到AI科技评论的推送。为了第一时间收到AI科技评论的报道，请将“AI科技评论”设为星标账号，以及常点文末右下角的“在看”。