2007图灵奖得主离开了：模型检测先驱Edmund Clarke因新冠逝世
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 年不会更糟糕了。」
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 年不会更糟糕了。」
