2007图灵奖得主离开了：模型检测先驱EdmundClarke因新冠逝世
  12月23日，英特尔量子硬件研究组总监JamesS.Clarke发文表示，他的父亲、2007年图灵奖得主EdmundM.Clarke因感染新冠不幸去世，享年75岁。
  EdmundM.Clarke生前就职于卡内基梅隆大学（CMU），是该校的终身教授。1981年，他与自己的博士生AllenEmerson首次提出了模型检测的想法并用在自动机并发系统的验证研究上，成为形式逻辑研究方面模型检测（modelchecking）的开创者之一。模型检测是一种自动验证技术，主要通过显式状态搜索或隐式不动点计算来验证有穷状态并发系统的模态/命题性质。
  
  由于模型检测可以自动执行，并能在系统不满足性质时提供反例路径，因此在工业界比演绎证明更受推崇。尽管限制在有穷系统上是一个缺点，但模型检测可以应用于许多非常重要的系统，如硬件控制器和通信协议等有穷状态系统。很多情况下，可以把模型检测和各种抽象与归纳原则结合起来验证非有穷状态系统（如实时系统）。
  
  作为这一领域的先驱，Clarke不仅开创了模型检测技术，还使之成为一个广泛应用在硬件和软件工业中非常有效的算法验证技术，并因此获得2007年的图灵奖。
  
  对于Clarke的不幸离世，CMU校长FarnamJahanian表示了沉痛悼念：「EdClarke离开了，这个世界又失去了一位计算机科学领域的巨人，此时CMU要向这位我们深爱的成员告别。Ed在模型检测方面的开拓性工作将形式化的计算方法应用于终极挑战：让计算机检查自身的正确性。随着系统变得越来越复杂，我们才刚刚认识到Ed的洞察所带来的广泛而深远的益处，这将在未来数年持续激励研究人员和从业人员前行。」
  
  生平回顾
  
  和很多计算机领域的大牛一样，EdmundClarke本科阶段学的并不是计算机，而是更为基础性的学科——数学。由于热爱计算机，他博士阶段选择了康奈尔大学的计算机专业，并于1976年拿到博士学位。
  
  本科期间的学习为EdmundClarke后来的研究打下了坚实的数学基础。他从自己感兴趣的领域——推理和可计算实数出发，首先着手于实数的非线性问题。1981年，他与自己的博士生首次提出模型检测的想法，并用在自动机并发系统的验证研究上，主要使用SAT验证完成模型检测，针对有界模型。
  
  然而从理论推导到实际工程应用是有距离的，因为实际系统大多都是混合系统，尤其是数值方法直接的使用会出现许多错误。为此，EdmundClarke的团队针对他们的思想开发出了dReal实用工具，该工具主要利用DPLL、间隔算法、限制性算法等思想研究实际问题。实际中，信息物理系统是一个庞大的系统，对于系统安全性问题的研究至关重要。针对这一研究目标，EdmundClarke团队验证了无人驾驶汽车、心脏模拟仿真等问题。
  
  在加入CMU计算机系之前，EdmundClarke曾在杜克大学和哈佛大学任教，还是计算机辅助验证会议的创始人之一，以及《系统设计形式方法》杂志的前主编。1989年，EdmundClarke被评为CMU全职终身教授。
  1995年，Clarke成为第一位获得FORESystems教授职位的人，并于2008年被任命为UniversityProfessor，这是CMU的最高教师荣誉。他是1998年ACMKanellakis奖、1999年AllenNewell杰出研究奖、2004年IEEEHarryH.Goode纪念奖和自动证明会议2008年Herbrand奖自动推理杰出贡献奖的获奖者。2014年，富兰克林研究所向Clarke颁发了鲍尔科学成就奖，以表彰他在计算机系统验证技术的概念和开发方面的引领作用。
  
  曾和Clarke在CMU共事的计算机科学家RandalE.Bryant这样介绍他：「EdClarke是一位杰出的研究者，同时是一个善良、充满爱心的人。我非常钦佩他指导博士生和博士后研究人员的能力，其中许多人通过自己的学术研究影响了全