巨星陨落！2007年图灵奖得主edmund clarke因感染新冠离世...
冬至刚过，不少人选择这一天祭奠先祖。过去的一年，无论是否因为新冠疫情，国内外各界都失去了许多我们熟悉的面孔。
例如，80后熟悉的春晚第一代主持人，赵忠祥老师。
还有传奇赌王何鸿燊。
喜欢NBA的朋友们自然不会忘记，那位永远的24号、永远的黑曼巴，科比。
漫威迷们也痛失了“黑豹”查德维克·博斯曼。
而几天前，让计算机界感到特别遗憾的是，当地时间12月22日，2007年图灵奖得主，美国著名计算机专家，爱德蒙·克拉克（Edmund M. Clarke）因感染新冠肺炎不幸离世，享年75岁。
在他去世的第二天，他的儿子，也是英特尔实验室量子硬件研究组的总监，詹姆斯·S·克拉克（James S. Clarke）在社交媒体上发布了这一消息。
或许，对于圈外人来说，这个名字并不为人所知。
爱德蒙·克拉克于1982年作为教授加入卡耐基梅隆大学计算机科学系；在此之前，他在杜克大学和哈佛大学任教，并获得了杜克大学的数学硕士学位及康奈尔大学的计算机博士学位，1989年被评为全职终身教授。
他是计算机辅助验证会议的创始人之一，也是ACM和IEEE会士，同时担任过Formal Methods in Systems Design杂志的主编。他在软硬件验证、自动定理证明、形式方法等领域享有崇高的国际声誉，是模型检测方法的开创者之一。
2007年，克拉克教授与艾伦·爱默生教授（Allen Emerson）和约瑟夫·斯发基斯（Joseph Sifakis）共同获得了被誉为计算科学领域诺贝尔奖的图灵奖。获奖原因是他们开发的模型检测技术，这是一种广泛应用于硬件和软件工业中的有效算法验证技术。
自计算机诞生以来，工程师们通过模拟运行来测试性能，并通过手动检查每一行代码来检测计算机电路或软件程序中的逻辑错误。但随着计算机软件和系统的日益复杂化，这些“非正式验证”的方法显然无法很好地解决问题。而克拉克教授等人的模型检测技术，可以有效分析设计背后的逻辑，就像数学家用证明来确定一个定理是正确的一样。模型检测能够考虑到硬件和软件设计的每种可能状态，并确定它是否与设计规范一致。可以说，克拉克教授他们的发明极大地减少了在产品发布后才发现错误所造成的昂贵代价，推动了整个计算机行业的发展。
对于克拉克教授的离世，卡耐基梅隆大学校长法纳姆·贾哈尼安（Farnam Jahanian）表示，“随着爱德蒙·克拉克的离世，世界失去了一位计算机科学界的巨人，卡耐基梅隆大学也告别了一位受人爱戴的成员”。卡耐基梅隆大学计算机科学学院院长马蒂尔·赫伯特（Martial Hebert）也表示，“治学严谨是爱德蒙·克拉克的一大特点，这为他赢得了计算机科学界的最高荣誉，也贯穿了他30多年的计算机科学生涯。”
同时，克拉克教授还是一位与中国颇有渊源的大师，他曾于2013年4月受邀出席清华大学“巅峰对话”，并在活动中介绍自己的学术历程和主要学术成果。当时他表示，正是出于对计算机的热爱，博士研究期间他从数学专业转到了计算机专业。不知道有多少清华学子在那次活动后义无反顾地改学了计算机。而前微软全球执行副总裁陆奇，在复旦大学取得硕士学位后，选择留校任教，正是在一次克拉克教授的演讲中与其相识，最终赴卡耐基梅隆大学就读，并于1996年5月毕业，获得了计算机科学博士学位。
克拉克教授还曾获得过ACM Kanellakis奖（1998年）、Allen Newell卓越研究奖（1999年）、IEEE Harry H. Goode纪念奖（2004年）、Herbrand奖（2008年）。1995年成为第一个拥有FORE Systems教授资格的人，2005年当选美国工程院院士，2008年升任卡耐基梅隆大学教师最高荣誉University Professor，2011年当选美国艺术和科学院院士。2014年，富兰克林学会向他颁发了鲍尔科学成就奖，以表彰他在计算机系统验证技术的构思和开发方面的领导作用。
新冠就这样带走了一位计算机界的巨人，或许是因为上帝在有人和他打篮球之后，又想有人教他用计算机吧，教授一路走好！
2020年Spring Cloud发布了最后一个大版本！
2020-12-24
支持Dubbo接口文档生成的工具！
2020-12-24
36张图梳理Intellij IDEA常用设置
2020-12-23
13个Mongodb GUI可视化管理工具，总有一款适合你
2020-12-23
小宇宙爆发！Spring Boot新特性：节省95%内存占用
2020-12-22
扫一扫，关注我
知晓前沿科技，领略技术魅力
DD自研的沪牌代拍业务
﹀
﹀
﹀
深度交流
