2007年图灵奖的共同获得者埃德蒙·克拉克（Edmund M.Clarke）死于Covid-19的12月22日

-卡内基梅隆大学名誉教授，2007年图灵奖的共同获得者埃德蒙·M·克拉克（Edmund M. Clarke）因长期病逝于12月22日死于COVID-19，该年的计算机科学相当于诺贝尔奖。

Clarke与他的哈佛大学研究生E. Allen Emerson以及格勒诺布尔大学的Joseph Sifakis一起工作，开发了一种自动方法来检测计算机硬件和软件中的设计错误。它被称为模型检查，已被广泛使用并有助于提高复杂计算机芯片，系统和网络的可靠性。计算机科学协会（ACM）将图灵奖授予了这三位科学家。

随着埃德·克拉克（Ed Clarke）的逝世，世界失去了计算机科学领域的巨人，CMU向我们社区中心爱的成员说再见，＆＃34;卡内基梅隆大学校长法纳姆·哈哈尼安（Farnam Jahanian）说。 Ed在模型检查中的开拓性工作将形式化的计算方法应用于最终的挑战：计算机检查自己的正确性。随着系统变得越来越复杂，我们才刚刚开始看到Ed's见解的广泛而长期的收益，这将在​​未来几年继续激发研究人员和从业人员的灵感。

自从计算开始以来，工程师就通过运行仿真来测试性能并通过手动检查每行计算机代码来检查计算机电路或软件程序中的逻辑错误。但是，随着计算机芯片上组件的数量呈几何级增长，并且随着软件和计算机系统变得越来越复杂，这些“偶然或失败”的“非正式验证”也就成为现实。方法证明不充分。直到产品发布后，错误通常才被发现，而纠正即使是很小的错误也是很昂贵的。

相比之下，模型检查是“形式验证”的一种。它分析了设计的逻辑基础，就像数学家使用证明来确定一个定理是正确的一样。模型检查绝不会碰碰运气，它会考虑硬件或软件设计的每种可能状态，并确定其是否符合设计者的规格。

＆＃34;严谨的思想是Ed Clarke的标志。它为他赢得了计算机科学的最高荣誉，并通过他为计算机科学系注入了30多年的经验，卡内基梅隆大学计算机学院院长Martial Hebert说。 ＆＃34;对于教师和学生而言，他都是一个光辉的榜样，我们所有人都很想念他。＆＃34;

克拉克（Clarke）获得博士学位。 1976年，他在康奈尔大学获得计算机科学博士学位。在1982年加入CMU的计算机科学系之前，他先后在杜克大学和哈佛大学任教，他的研究小组继续在形式验证和自动定理证明方面担任先驱。他是计算机辅助验证会议的创始人之一，并且是《系统设计形式方法》杂志的前主编。

＆＃34;埃德·克拉克（Ed Clarke）是一位出色的研究人员，但也是一位善良而充满爱心的人，＆＃34;创始人大学计算机科学荣誉教授Randal E. Bryant说。 ＆＃34;我特别钦佩他指导博士的能力。学生和博士后研究人员，其中许多人通过他们的研究对世界产生了重大影响。＆＃34;

1995年，克拉克（Clarke）成为第一位获得FORE Systems教授资格的人，并于2008年被任命为CMU的最高教授荣誉大学教授。他是1998年ACM Kanellakis奖，1999年Allen Newell杰出研究奖，2004年IEEE哈里·古德纪念奖和自动扣除会议2008年Herbrand杰出贡献奖的共同获奖者。推理。 2014年，富兰克林研究所向他颁发了鲍尔奖和科学成就奖，以表彰他在计算机系统验证技术的概念和开发方面的领导作用。

他由妻子玛莎（Martha）幸存下来，妻子玛莎是计算机科学系和计算机科学学院的研究生招生协调员，直到2014年退休。他还由俄勒冈州波特兰市的三个儿子詹姆斯·克拉克（James Clarke）幸存下来；乔治亚州迪凯特市的乔纳森·克拉克（Jonathan Clarke）和北卡罗来纳州达勒姆市的杰弗里·克拉克博士以及六个孙子。

劳恩林纪念教堂（Laughlin Memorial Chapel）正在安排私人葬礼服务。黎巴嫩一家人要求向山顶捐款。黎巴嫩联合卫理公会教堂食品储藏室，宾夕法尼亚州匹兹堡西自由区3319号，宾夕法尼亚州15216，并向埃德蒙和玛莎·克拉克授予计算机科学学院研究生奖学金。