[指南] 2007年图灵奖获得者Edmund M. Clarke不幸于当地时间12月22日去世，原因是他患上了新的冠状肺炎。

当地时间12月22日，2007年图灵奖得主埃德蒙·克拉克（Edmund M. Clarke）死于COVID-19，享年75岁。

他的儿子詹姆斯·克拉克（James Clarke）在Twitter上发布了这一消息。

詹姆斯·克拉克（James Clarke）在一条推文中说：“今天，我的父亲埃德蒙·克拉克（Edmund M. Clark）死于新的冠心病。

他曾获得2007年图灵奖。

我父亲一直对我的学术研究寄予厚望，并且还教我打棒球，钓鱼，环游世界。

我会非常想念他的”。

据了解，詹姆斯·克拉克（James Clarke）目前是英特尔量子硬件研究小组的主任。

Clark教授一生中一直专注于软件和硬件系统的验证以及自动理论证明的研究。

在他的博士论文中，有一项工作来证明某些编程语言的控制逻辑中没有完美的Hoare理论证明系统。

教授一生埃德蒙·克拉克（Edmund Clark）于1945年出生，1967年获得弗吉尼亚大学数学学士学位。

1976年，康奈尔大学获得了博士学位。

来自计算机科学系。

1982年，克拉克教授加入了卡内基梅隆大学的计算机科学系。

在此之前，他曾在杜克大学和哈佛大学任教，他的研究小组继续在形式验证和自动定理证明方面开创先河。

他是计算机辅助验证会议的创始人之一，并且还是《 FormalMethodsinSystemsDesign》杂志的主编。

1995年，克拉克（Clark）成为第一位获得FORESystems教授资格的人。

2008年，他被提升为大学教授，这也是CMU老师的最高荣誉。

他于1998年获得了ACMKanellakis奖，于1999年获得了AllenNewell研究卓越奖，于2004年获得了IEEEHarryh.Goode纪念奖，并在2008年的自动推理演绎大会上获得了Herbrand杰出贡献奖（共同获奖）。

2014年，他获得了ACMKanellakis奖。

富兰克林研究所授予他“科学成就奖”，以表彰他在计算机系统验证技术的概念和开发方面的领导地位。

他被选为CMU的名誉教授，2015年谁教计算机检查错误都不见了的人。

自计算机诞生以来，工程师就通过运行仿真来测试性能或手动检查每行计算机代码来检查计算机电路或软件程序中的逻辑错误。

但是，随着计算机芯片上组件的数量成倍增加，软件和计算机系统也变得更加复杂。

这些偶然的“非正式验证”会在不安全的情况下发生。

方法显然是不够的。

通常会在产品发布后发现错误，因为即使是很小的错误，纠正起来也非常昂贵。

1981年，时任哈佛大学助理教授的克拉克与格勒诺布尔大学的研究生E. Allen Emerson和Joseph Sifakis一起开发了一种自动检测计算机硬件和软件设计错误的方法，称为模型检查。

模型检查是一种“形式验证”。

就像数学家使用证明来确定一个定理是正确的一样，它分析了设计背后的逻辑。

模型检查会考虑硬件或软件设计的每种可能状态，并确定其是否与设计者的规范一致，从而极大地避免了意外错误。

随后，它被广​​泛用于帮助提高复杂计算机芯片，系统和网络Sex的可靠性。

Clark教授和E.Allen Emerson教授Joseph Sifakis为此获得了2007年图灵奖。

卡内基·梅隆大学（Carnegie Mellon University）校长Farnam Jahanian说：“爱德华（Ed）在模型检查中的开拓性工作将形式化的计算方法应用于最终挑战：计算机检查其正确性。

随着系统变得越来越复杂，我们才刚刚开始看到Ed的见解所带来的广泛和长期的收益，这将在​​未来几年继续激发研究人员和从业人员的灵感”。

新的王冠夺走了克拉克教授，世界失去了另一个计算机巨人。

但是，教授，天堂再好不过了！