北京12月23日上午，2007年图灵奖得主、计算机科学家爱德蒙·克拉克（Edmund Clarke）因感染新冠肺炎不幸逝世，享年75岁。

克拉克生前是美国卡内基梅隆大学的名誉教授。他以从事模型检测方面的工作而闻名世界。模型检测是一种自动验证技术，可以自动检测计算机软硬件的设计错误，有助于提高计算机系统的准确性和可靠性。

克拉克出生于美国维吉尼亚州，在求学时先后获得数学学士、数学硕士及计算机博士学位。他于1978年加入哈佛大学担任助理教授，1982年离开哈佛、进入卡内基梅隆大学计算机科学系。1989年，他被评为卡内基梅隆大学全职终身教授。

1981年在哈佛大学任教期间，克拉克与他的博士生艾伦·爱默生（Allen Emerson）、法国学者约瑟夫·斯发基斯（Joseph Sifakis）合作，首次提出模型检测的想法。

模型检测技术问世后，成为分析验证并发系统性质的最重要的技术之一，并被英特尔、IBM、微软等公司广泛应用于生产实践中。2007年，克拉克、爱默生与斯发基斯获得图灵奖。

克拉克的著作《模型检测》中文版于2018年出版，书中涵盖的内容包括模型检测的基本知识、符号化技术、抽象解释、程序分析等等。

值得注意的是，克拉克还曾担任中国科学院“爱因斯坦讲席教授”。2013年，他来到北京，在中国科学院软件研究所做了三场学术报告，介绍了模型检测技术在软件、信息物理融合系统、生物信息学等领域的应用前景。

2013年，克拉克还在清华大学参加了一场“巅峰对话”活动。被问及如何保持对科研的积极心态，他表示，他对于喜欢的东西有一种着了魔的热情，喜欢拼尽全力解决问题；在时间安排上，他会给科研工作留出充足的余量，避免自己过度陷入行政工作中。

对于克拉克的不幸离世，卡内基梅隆大学校长法纳姆·翰尼安（Farnam Jahanian）悼念称，“这个世界又失去了一位计算机科学领域的巨人。我们才刚刚认识到克拉克的见解所带来的广泛而深远的益处，这将在未来数年中持续激励研究人员和从业人员前行。”

“克拉克是一位杰出的研究者，与此同时也是一位和蔼友爱的老师。”卡内基梅隆大学计算机科学系荣誉教授兰德尔·布莱恩特（Randal E. Bryant）坦言，“我特别钦佩他指导博士生和博士后研究人员的能力。其中很多人凭借他们的研究在全世界范围产生了重大的影响。”

克拉克的儿子詹姆斯·克拉克（James S.Clarke）如今是英特尔实验室量子硬件研究组总监。他发文表示，父亲不仅对他的学术研究寄予厚望，同时还教他打棒球、钓鱼、环球旅行。“我将深切地怀念他。”

世界各地的网友也表达了对克拉克的悼念。

综合：南都人工智能伦理课题组研究员 靳忠骥 冯群星

编辑：冯群星