巨星陨落!图灵奖得主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

— 完 —

(0)

相关推荐