图灵奖得主克拉克感染新冠逝世

图灵奖得主克拉克感染新冠逝世 图灵奖得主爱德蒙·克拉克（Edmund M. Clarke）因感染新冠肺炎不幸去世，享年75岁。他的儿子 James Clarke （英特尔量子硬件研究组总监）在推特上发布了这一消息。

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

但是，随着计算机芯片上组件的数量呈几何级数增长，软件和计算机系统同样也变得更加复杂，这些偶然的「非正式验证」方法显然是不够的。

错误通常在产品发布后才被发现，因为即使是微小的错误就整起来也非常昂贵的。

1981年，当时在哈佛担任助理教授的克拉克与他的研究生E. Allen Emerson以及Grenoble大学的Joseph Sifakis，开发了一种自动检测计算机硬件和软件设计错误的方法，被称为模型检测。三人因此获得了2007年的图灵奖。

模型检测是一种分析设计背后逻辑的「形式验证」，就像数学家使用证明来确定一个定理是正确的。

模型检测考虑硬件或软件设计的每一种可能状态，并确定它是否与设计者的规范一致，大大避免了偶然错误的出现，随后它被广泛应用，帮助提高复杂计算机芯片、系统和网络的可靠性。