2007年图灵奖得主因感染新冠肺炎去世，享年75岁

　　当地时间12月23日，英特尔实验室量子硬件研究组总监James S. Clarke在社交媒体发文表示，他的父亲、2007年图灵奖得主爱德蒙·克拉克(Edmund M. Clarke)因感染新冠肺炎不幸去世。

　　爱德蒙·克拉克曾任美国卡耐基梅隆大学计算机科学系教授，是ACM和IEEE会士。他在软硬件验证、自动定理证明、形式方法等方面享有崇高的国际声誉，是模型检测方法的开创者之一。对于爱德蒙·克拉克的离世，卡耐基梅隆大学校长Farnam Jahanian表示，“随着爱德蒙·克拉克的去世，世界失去了一位计算机科学界的巨人，卡耐基梅隆大学也告别了一位受人爱戴的成员”。他说，目前学术界才刚刚开始看到爱德蒙在模型检测方面的开创性工作所带来的广泛且长期的益处，他的见解在未来几年还会继续激励研究人员和从业者。

因开发模型检测技术获图灵奖

　　爱德蒙·克拉克出生于1945年，1967年在弗吉尼亚大学获得数学学士学位，1968年在杜克大学获得数学硕士学位，1976年在康奈尔大学获得计算机博士学位。然后，克拉克教授在杜克大学任教两年，于1978年加入哈佛大学并担任助理教授。1982年，加入卡耐基梅隆大学计算机系。

　　2007年，爱德蒙·克拉克与艾伦·爱默生教授(Allen Emerson)和约瑟夫·斯发基斯(Joseph Sifakis)共同获得图灵奖，该奖项有计算机科学领域的“诺贝尔奖”之称。获奖理由是他们开发了模型检测技术，并使之成为一个广泛应用在硬件和软件工业中非常有效的算法验证技术。

　　自计算机诞生以来，工程师们通过模拟运行来测试性能，并通过手动检查每一行代码来检测计算机电路或软件程序中的逻辑错误。但随着计算机软件和系统日益复杂化，这些“非正式验证”的方法显然无法很好地解决问题。

　　相比之下，爱德蒙·克拉克等人开发的模型检测技术可以分析设计背后的逻辑，就像数学家用证明来确定一个定理是正确的一样。模型检测能够考虑到硬件和软件设计的每种可能状态，并确定它是否与设计规范相一致。

　　1981年，爱德蒙·克拉克与自己的博士生首次提出模型检测的想法，并用在自动机并发系统的验证研究上，主要使用SAT验证完成模型检测，主要针对于有界模型。然而从理论推导到实际工程应用是有距离的，因为实际系统大多都是混合系统，尤其是数值方法直接的使用会出现许多错误。为此，爱德蒙教授的团队针对他们的思想开发出了dReal实用工具，该工具主要利用DPLL、间隔算法、限制性算法等思想研究实际问题。

晚年仍记得自己的第一台计算机

　　卡耐基梅隆大学计算机科学学院院长Martial Hebert表示，治学严谨是爱德蒙·克拉克的一大特点，这为他赢得了计算机科学界的最高荣誉，也贯穿了他30多年的计算机科学生涯。

　　2013年4月，爱德蒙·克拉克在受邀出席清华大学“巅峰对话”活动时介绍过自己的学术历程和主要学术成果。据清华大学新闻网报道，出于对计算机的酷爱，博士研究期间爱德蒙·克拉克从数学专业转到计算机专业。本科期间的学习为后来的研究打下了坚实的数学基础。

　　在那次演讲中，爱德蒙·克拉克强调了数学基础训练之于计算机研究的重要性。他说，“计算是一件令人兴奋的事情，数学则是做好计算机科学的关键，数学的各种算法本质上是培养一种思维方式，这对于本科生无疑是很好的一个专业。”

　　爱德蒙·克拉克还是前微软全球执行副总裁陆奇的伯乐。据媒体报道，陆奇1987年在复旦大学取得硕士学位后，选择留校任教。一次，他去听爱德蒙·克拉克的演讲，在会场上以自己的问题征服了克拉克邀请他前往卡耐基梅隆大学读书。后来，陆奇赴卡耐基梅隆大学读书并于1996年5月毕业，获得计算机科学博士学位。

　　2015年，爱德蒙·克拉克成为卡耐基梅隆大学的荣誉退休教授(emeritus professor)。退休以后，克拉克一直住在位于美国匹兹堡的养老院中，并患上了老年痴呆症。他的儿子James S. Clarke曾表示，尽管父亲患有晚年老年痴呆症，却仍能够回忆起自己的第一台计算机。

　　爱德蒙·克拉克曾获IEEE Harry M. Goode纪念奖(2004年)，Herbrand奖(2008年)。2005年当选美国工程院院士，2011年当选美国艺术和科学院院士。