又一位巨星因新冠陨落，07年图灵奖得主Edmund Clarke，享年75岁

　　又一位巨星陨落！

　　据最新消息，2007年图灵奖得主、计算机科学家Edmund Clarke，因感染新冠肺炎，于北京时间12月23日上午不幸逝世。

　　其子James S。 Clarke在Twitter发文公布此消息之余，也悼念道：虽然他对（我）学业上的成功总是抱有很高的期望，但他也教会了我打棒球、钓鱼和环游世界。我将深深地怀念他。

　　对此，中国科学院大学教授包云岗表示：享年75岁，人类的损失！

　　网友们在表达哀悼的同时，也给予了Edmund高度的认可：如果没有他的贡献，很难想象我的领域会是什么样子。

　　他对科学的贡献是无法估量的。

　　Edmund Clarke：“软件和硬件验证”先驱

　　Edmund出生于1945年7月27日。

　　根据维基百科的介绍，他于1967年弗吉尼亚大学获得数学学士学位；次年，在杜克大学拿到了数学硕士学位。

　　1976年，Edmund于康奈尔大学获得了计算机科学博士学位。

　　此后，他先是在杜克大学计算机科学系任教2年，并于1978年转到了哈佛大学，担任应用科学系计算机科学助理教授。

　　1982年，离开哈佛大学的他，又来到了卡内基梅隆大学计算机科学系任教。

　　7年后，也就是1989年，Edmund 被任命为正教授。

　　值得注意的是，他是CMU计算机科学学院FORE Systems Professorship的第一位获得者。

　　根据维基百科所述，Edmund所擅长的研究包括“软件和硬件验证”以及“自动定理证明”。

　　早在他的博士论文中，便证明了：某些编程语言控制结构没有良好的Hoare式证明系统。

　　1981年，Edmund和他的博士生E。 Allen Emerson，首次提出使用模型检查作为有限状态并发系统的验证技术。他的研究小组率先将模型检查用于硬件验证。

　　使用二元决策图（binary decision diagram）的符号模型检查，也是由他的研究小组开发。

　　这一重要技术是Kenneth McMillan的博士论文的主题，该论文还获得了ACM博士论文奖。

　　此外，他的研究小组还开发了第一个并行解析定理推理器（Parthenon）和第一个基于符号计算系统的定理推理器（Analytica）。

　　2007年，他与Ernest Allen Emerson和Joseph Sifakis一起，因在模型检查方面取得的杰出贡献而获得图灵奖。

　　也正因Edmund在该领域中的杰出贡献，他还斩获了ACM Paris Kanellakis奖、赫布兰奖、美国国家工程院院士等荣誉和头衔。

　　Edmund还是中国科学院“爱因斯坦讲席教授”，在2013年10月在中国科学院进行过访问交流。

图源：中国科学软件研究所

　　其他巨星的陨落

　　对计算机领域做出如此杰出贡献者，因疫情而逝世实属令人惋惜。

　　这无疑是“人类的损失”。令人更为痛心的是，回看“黑天鹅”袭来的这一年，还有太多因新冠而陨落的巨星。

　　4月12日，当代最有趣的数学家John Horton Conway，因为新冠肺炎逝世，享年82岁。

　　有人评价他，世界上可能有比他更厉害的数学家，但是在顶尖的数学家里，没有人能比他科普做得更好。

　　他在数学领域多点开花，是一个在组合博弈论、几何、数论、群论、算法甚至量子力学理论等多个方面都做出贡献的天才数学家。

　　2月15日，华中科技大学教授、中国工程院院士著名机械工程专家段正澄因感染新冠肺炎去世，享年86岁。

　　段院士生前一直工作在一线，与生产紧密结合，致力于国家重要需求的自动化、数字化加工技术与装备的应用基础研究和工程技术研发。

　　段院士获得过国家科学技术进步一等奖1项、二等奖3项。其中二等奖的3项成果，没有哪一项少于10年：研制全身伽玛刀，10年；研究激光加工技术与装备，20年；完善汽车发动机曲轴磨床，30年。

　　……

　　他们对科学、对人类所创造出来的价值，用“无价”来形容并不为过。

　　应当值得被后人谨记和尊重，不仅仅是卓越的贡献和事迹，更是他们所秉持的对科学的精神。