12 月 23 日，英特尔量子硬件钻研组总监 James S. Clarke 发文表示，他的父亲、2007 年图灵奖得主 Edmund M. Clarke 因感染新冠不幸去世，享年 75 岁。
Edmund M. Clarke 生前就职于卡内基梅隆大学（CMU），是该校的终身传授。1981 年，他与自己的博士生 Allen Emerson 首次提出了模型检测的想法并用在主动机并发体系的考证钻研上，成为形式逻辑钻研方面模型检测（model checking）的开创者之一。模型检测是一种主动考证手艺，主要通过显式形态搜索或隐式不动点计算来考证有穷形态并发体系的模态 / 命题性质。由于模型检测可以主动执行，并能在体系不满足性质时提供反例路径，因此在工业界比演绎证明更受推崇。尽管限制在有穷体系上是一个缺点，但模型检测可以应用于许多非常重要的体系，如硬件控制器和通信协议等有穷形态体系。很多情况下，可以把模型检测和各种抽象与归纳原则结合起来考证非有穷形态体系（如实时体系）。作为这一领域的先驱，Clarke 不仅开创了模型检测手艺，还使之成为一个广泛应用在硬件和软件工业中非常有效的算法考证手艺，并因此获得 2007 年的图灵奖。对于 Clarke 的不幸离世，CMU 校长 Farnam Jahanian 表示了沉痛悼念：「Ed Clarke 离开了，这个世界又失去了一位计算机科学领域的巨人，此时 CMU 要向这位我们深爱的成员告别。Ed 在模型检测方面的开拓性工作将形式化的计算方法应用于终极挑战：让计算机检查自身的正确性。随着体系变得越来越复杂，我们才刚刚认识到 Ed 的洞察所带来的广泛而深远的益处，这将在未来数年持续激励钻研人员和从业人员前行。」生平回顾和很多计算机领域的大牛一样，Edmund Clarke 本科阶段学的并不是计算机，而是更为基础性的学科——数学。由于热爱计算机，他博士阶段选择了康奈尔大学的计算机专业，并于 1976 年拿到博士学位。本科期间的学习为 Edmund Clarke 后来的钻研打下了坚实的数学基础。他从自己感兴趣的领域——推理和可计算实数出发，首先着手于实数的非线性题目。1981 年，他与自己的博士生首次提出模型检测的想法，并用在主动机并发体系的考证钻研上，主要使用 SAT 考证完成模型检测，针对有界模型。然而从理论推导到现实工程应用是有距离的，因为现实体系大多都是混合体系，尤其是数值方法直接的使用会出现许多错误。为此，Edmund Clarke 的团队针对他们的思想开发出了 dReal 实用工具，该工具主要利用 DPLL、间隔算法、限制性算法等思想钻研现实题目。现实中，信息物理体系是一个庞大的体系，对于体系安全性题目的钻研至关重要。针对这一钻研目标，Edmund Clarke 团队考证了无人驾驶汽车、心脏模拟仿真等题目。在加入 CMU 计算机系之前，Edmund Clarke 曾在杜克大学和哈佛大学任教，还是计算机辅助考证会议的创始人之一，以及《体系设计形式方法》杂志的前主编。1989 年，Edmund Clarke 被评为 CMU 全职终身传授。1995 年，Clarke 成为第一位获得 FORE Systems 传授职位的人，并于 2008 年被任命为 University Professor，这是 CMU 的最高教师荣誉。他是 1998 年 ACM Kanellakis 奖、1999 年 Allen Newell 卓异钻研奖、2004 年 IEEE Harry H. Goode 纪念奖和主动证明会议 2008 年 Herbrand 奖主动推理卓异贡献奖的获奖者。2014 年，富兰克林钻研所向 Clarke 颁发了鲍尔科学成就奖，以表彰他在计算机体系考证手艺的概念和开发方面的引领作用。曾和 Clarke 在 CMU 共事的计算机科学家 Randal E. Bryant 这样介绍他：「Ed Clarke 是一位卓异的钻研者，同时是一个善良、充满爱心的人。我非常钦佩他指导博士生和博士后钻研人员的能力，其中许多人通过自己的学术钻研影响了全世界。」除了培养人才方面的卓异能力，Clarke 在发现人才方面也是慧眼独具，前百度副总裁、现奇绩创坛创始人兼 CEO 陆奇便是他发现的人才之一。他免去了陆奇「45 美元的申请手续费」对于陆奇来说，Clarke 是「伯乐」一般的存在。
上世纪 80 年代末，陆奇刚刚在复旦大学计算机系读完本科和钻研生，并留校任教。Edmund Clarke 受邀来到复旦讲课，对陆奇在其研讨会上提出的题目产生了深刻印象。会后，Edmund Clarke 看了陆奇的论文，随后邀请他申请 CMU 的博士项目。得知在大学任教的陆奇月薪仅有几十元人民币，Clarke 免去了 45 美元的申请手续费并提供了奖学金。1996 年，陆奇获得了卡内基梅隆大学的计算机博士学位。退休以后，Clarke 一直住在匹兹堡的养老院。尽管已经患上老年痴呆症，但他仍然能够回忆起自己的第一台计算机。
当 Clarke 去世的消息传来，曾经的学生、威斯康辛大学麦迪逊分校传授 Somesh Jha 在推特上说：「感觉 2020 年不会更糟糕了。」
参考链接：https://www.cs.cmu.edu/news/edmund-clarke-pioneered-methods-detecting-software-hardware-errorshttps://news.tsinghua.edu.cn/info/1010/58633.htmhttps://baike.baidu.com/item/%E6%A8%A1%E5%9E%8B%E6%A3%80%E6%B5%8B/5628442http://m.gerenjianli.com/Mingren/03/o31ttbnps44logs.htmlhttps://www.cmu.edu/cmtoday/issues/october-2010-issue/feature-stories/bing-it-on/index.html
原创文章，作者：机器之心，如若转载，请注明出处：https://www.iaiol.com/news/2007-tu-ling-jiang-de-zhu-li-kai-le-mo-xing-jian-ce-xian-qu/
