2007图灵奖得主离开了：模型检测先驱Edmund Clarke因新冠逝世

嵌入式资讯精选 2020-12-27 00:00

【50份好礼】首发直播：解密Keysight最新模拟信号源 精密双向电流感应放大器设计方案

2020 还能更糟糕吗？

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 是「伯乐」一般的存在。