巨星陨落！图灵奖得主Edmund Clarke因新冠逝世
又一位巨星陨落！
据最新消息，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年。
……
他们对科学、对人类所创造出来的价值，用“无价”来形容并不为过。
应当值得被后人谨记和尊重，不仅仅是卓越的贡献和事迹，更是他们所秉持的对科学的精神。
参考链接：
https://zh.wikipedia.org/wiki/%E7%88%B1%E5%BE%B7%E8%92%99%C2%B7%E5%85%8B%E6%8B%89%E5%85%8B#cite_note-2
https://twitter.com/Jim_in_Oregon/status/1341546882321944576
http://www.iscas.ac.cn/xwdt2016/kjdt2016/201310/t20131022_3960865.html
— 完 —