又一位巨星陨落!

  据最新消息,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年。

  ……

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

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


新闻来源:新浪