2007图灵奖得主离开了:模型检测先驱Edmund Clarke因新冠逝世

2020 还能更糟糕吗?

12 月 23 日,英特尔量子硬件钻研组总监 James S. Clarke 发文表示,他的父亲、2007 年图灵奖得主 Edmund M. Clarke 因感染新冠不幸去世,享年 75 岁。

2007图灵奖得主离开了:模型检测先驱Edmund Clarke因新冠逝世

Edmund M. Clarke 生前就职于卡内基梅隆大学(CMU),是该校的终身传授。1981 年,他与自己的博士生 Allen Emerson 首次提出了模型检测的想法并用在主动机并发体系的考证钻研上,成为形式逻辑钻研方面模型检测(model checking)的开创者之一。模型检测是一种主动考证手艺,主要通过显式形态搜索或隐式不动点计算来考证有穷形态并发体系的模态 / 命题性质。由于模型检测可以主动执行,并能在体系不满足性质时提供反例路径,因此在工业界比演绎证明更受推崇。尽管限制在有穷体系上是一个缺点,但模型检测可以应用于许多非常重要的体系,如硬件控制器和通信协议等有穷形态体系。很多情况下,可以把模型检测和各种抽象与归纳原则结合起来考证非有穷形态体系(如实时体系)。作为这一领域的先驱,Clarke 不仅开创了模型检测手艺,还使之成为一个广泛应用在硬件和软件工业中非常有效的算法考证手艺,并因此获得 2007 年的图灵奖。对于 Clarke 的不幸离世,CMU 校长 Farnam Jahanian 表示了沉痛悼念:「Ed Clarke 离开了,这个世界又失去了一位计算机科学领域的巨人,此时 CMU 要向这位我们深爱的成员告别。Ed 在模型检测方面的开拓性工作将形式化的计算方法应用于终极挑战:让计算机检查自身的正确性。随着体系变得越来越复杂,我们才刚刚认识到 Ed 的洞察所带来的广泛而深远的益处,这将在未来数年持续激励钻研人员和从业人员前行。」生平回顾和很多计算机领域的大牛一样,Edmund Clarke 本科阶段学的并不是计算机,而是更为基础性的学科——数学。由于热爱计算机,他博士阶段选择了康奈尔大学的计算机专业,并于 1976 年拿到博士学位。本科期间的学习为 Edmund Clarke 后来的钻研打下了坚实的数学基础。他从自己感兴趣的领域——推理和可计算实数出发,首先着手于实数的非线性题目。1981 年,他与自己的博士生首次提出模型检测的想法,并用在主动机并发体系的考证钻研上,主要使用 SAT 考证完成模型检测,针对有界模型。然而从理论推导到现实工程应用是有距离的,因为现实体系大多都是混合体系,尤其是数值方法直接的使用会出现许多错误。为此,Edmund Clarke 的团队针对他们的思想开发出了 dReal 实用工具,该工具主要利用 DPLL、间隔算法、限制性算法等思想钻研现实题目。现实中,信息物理体系是一个庞大的体系,对于体系安全性题目的钻研至关重要。针对这一钻研目标,Edmund Clarke 团队考证了无人驾驶汽车、心脏模拟仿真等题目。在加入 CMU 计算机系之前,Edmund Clarke 曾在杜克大学和哈佛大学任教,还是计算机辅助考证会议的创始人之一,以及《体系设计形式方法》杂志的前主编。1989 年,Edmund Clarke 被评为 CMU 全职终身传授。1995 年,Clarke 成为第一位获得 FORE Systems 传授职位的人,并于 2008 年被任命为 University Professor,这是 CMU 的最高教师荣誉。他是 1998 年 ACM Kanellakis 奖、1999 年 Allen Newell 卓异钻研奖、2004 年 IEEE Harry H. Goode 纪念奖和主动证明会议 2008 年 Herbrand 奖主动推理卓异贡献奖的获奖者。2014 年,富兰克林钻研所向 Clarke 颁发了鲍尔科学成就奖,以表彰他在计算机体系考证手艺的概念和开发方面的引领作用。曾和 Clarke 在 CMU 共事的计算机科学家 Randal E. Bryant 这样介绍他:「Ed Clarke 是一位卓异的钻研者,同时是一个善良、充满爱心的人。我非常钦佩他指导博士生和博士后钻研人员的能力,其中许多人通过自己的学术钻研影响了全世界。」除了培养人才方面的卓异能力,Clarke 在发现人才方面也是慧眼独具,前百度副总裁、现奇绩创坛创始人兼 CEO 陆奇便是他发现的人才之一。他免去了陆奇「45 美元的申请手续费」对于陆奇来说,Clarke 是「伯乐」一般的存在。

2007图灵奖得主离开了:模型检测先驱Edmund Clarke因新冠逝世

上世纪 80 年代末,陆奇刚刚在复旦大学计算机系读完本科和钻研生,并留校任教。Edmund Clarke 受邀来到复旦讲课,对陆奇在其研讨会上提出的题目产生了深刻印象。会后,Edmund Clarke 看了陆奇的论文,随后邀请他申请 CMU 的博士项目。得知在大学任教的陆奇月薪仅有几十元人民币,Clarke 免去了 45 美元的申请手续费并提供了奖学金。1996 年,陆奇获得了卡内基梅隆大学的计算机博士学位。退休以后,Clarke 一直住在匹兹堡的养老院。尽管已经患上老年痴呆症,但他仍然能够回忆起自己的第一台计算机。

2007图灵奖得主离开了:模型检测先驱Edmund Clarke因新冠逝世

当 Clarke 去世的消息传来,曾经的学生、威斯康辛大学麦迪逊分校传授 Somesh Jha 在推特上说:「感觉 2020 年不会更糟糕了。」

2007图灵奖得主离开了:模型检测先驱Edmund Clarke因新冠逝世

参考链接:https://www.cs.cmu.edu/news/edmund-clarke-pioneered-methods-detecting-software-hardware-errorshttps://news.tsinghua.edu.cn/info/1010/58633.htmhttps://baike.baidu.com/item/%E6%A8%A1%E5%9E%8B%E6%A3%80%E6%B5%8B/5628442http://m.gerenjianli.com/Mingren/03/o31ttbnps44logs.htmlhttps://www.cmu.edu/cmtoday/issues/october-2010-issue/feature-stories/bing-it-on/index.html

原创文章,作者:机器之心,如若转载,请注明出处:https://www.iaiol.com/news/2007-tu-ling-jiang-de-zhu-li-kai-le-mo-xing-jian-ce-xian-qu/

(0)
上一篇 2020年 12月 23日 下午2:34
下一篇 2020年 12月 25日 下午7:20

相关推荐

  • 规模化机械学习崛起、「零断定」架构出现,德勤呈文2021九大技巧趋向

    《德勤2021年技巧趋向》呈文研究了疫情一年来对企业战术、运营和技巧带来的连锁反应,论述了其重大发现:全球企业在加速数字化战术转型,从而构建「韧性」、开创全新的经营模式。呈文讨论了接下来18至24个月及以后驱动企业规划背后的九大技巧趋向,包括现在的工作环境、人工智能产业化、关键外围业务的升级以及撑持多样性、公道性和包容性的技巧等内容。这些技巧趋向也同时明确了动荡一年所带来的更具希望的一面。日前,德勤管理咨询正式发布了《2021技巧趋向呈文》。本年度呈文研究了疫情一年来对企业战术、运营和技巧带来的连锁反应,论述了其

    2020年 12月 31日
  • 图神经网络精确预计有机化合物性质,加速静态电池的设计

    编辑/绿萝大规模从头较量争论与布局预计的进步相结合,在有机功能资料的发觉中发挥了重要作用。目前,在有机资料的广阔化学空间中,只发觉了一小部分。实验和较量争论研讨职员都需要加速探索未知的化学空间。来自美国国家可再生能源实验室(NREL)、科罗拉多矿业学院和伊利诺伊大学的研讨职员展示了一种可以精确预计有机化合物性质的机械进修方法。展示了基态(GS)和更高能量布局的平衡训练数据集,对使用通用图神经网络(GNN)架构精确预计总能量的重要性。该研讨可加速静态电池的设计。该研讨以「Predicting energy and stabi

    2021年 12月 24日
  • 94岁诺奖得主希格斯去世,曾预言「上帝粒子」的生存

    一名用诗意的语言揭示宇宙秘密的人。一名 94 岁平凡科学家的逝世,引发了人们广泛的哀思。4 月 10 日消息,诺贝尔物理学奖得主、著名物理学家彼得・希格斯(Peter Higgs)于周一去世,享年 94 岁。希格斯因提出希格斯玻色子也被称为「上帝粒子」而闻名。根据爱丁堡大学的一份声明我们得知(彼得・希格斯是该校的名誉退休传授),希格斯经历短暂的生病后,于 4 月 8 日星期一在家中安静的离开。对于老爷子的去世,爱丁堡大书院长 Peter Mathieson 沉重的表示:「彼得・希格斯是一名杰出的科学家 &mdash

    2天前
  • Snowflake如日中天是否代表Hadoop已死?大数据体系到底是什么?

    作者 | 阿里云计较平台研究员关涛、阿里巴巴项目管理专家王璀任何一种手艺都会经历从阳春白雪到下里巴人的过程,就像我们对计较机的理解从“戴着鞋套才能进的机房”变成了随处可见的智能手机。在前面20年中,大数据手艺也经历了这样的过程,从曾经高高在上的 “火箭科技(rocket science)”,成为了人人普惠的手艺。回首来看,大数据落后初期涌现了非常多开源和自研体系,并在同一个范畴展开了相当长的一段“红海”竞争期,例如Yarn VS Mesos、Hive VS Spark、Flink VS SparkStreaming

    2021年 8月 11日
  • ICLR 2022 | 鉴于心智理论的多智能体通讯与分工

    本文是 ICLR 2022入选论文《ToM2C: Target-oriented Multi-agent Communication and Cooperation with Theory of Mind》的解读。该论文由北京大学王亦洲课题组完成。文章提出了一种鉴于心智理论的多智能体通讯与分工方法。每一个智能体鉴于对他人心理状态的推想独立地抉择通讯对象和个体行动,进而实现分布式的分工。试验表明该方法提高了多智能体分工的成功率,大幅降低了通讯价钱,并且具有良好的泛化性能。

    2022年 7月 18日
  • 百分点大数据技术团队:数据管理“PAI”实施方法论

    编者按数据作为第五大生产要素,已逐渐成为政府和企业决策的重要手段与依据。面对数据多样化、数据需要个性化、数据应用智能化的需要,以及在2B和2G行业中数据品质参差不齐、数据应用难以发挥价值、数据资产难以积淀等问题,如何做好数据管理事务、提拔数据管理才智成为了政府和企业数字化转型的重中之重。百分点大数据技术团队基于多年的数据管理项目经验,总结了一套做好数据管理事务及提拔数据管理才智的实施方法论。近年来,推动数据管理体系建设一直是业界探索的热点,另外,《中共中央、国务院关于构建更加完善的要素市场化配置体制机制的意见》将数

    2021年 3月 10日
  • 对抗图象变幻进犯,腾讯OVB-AI手艺中心获NeurIPS2021图象近似度寻衅赛季军

    近日,在 AI 顶会 NeurIPS 2021 的图象近似度寻衅赛中(Image Similarity Challenge),来自腾讯在线视频 BU-AI 手艺中心的团队,在 Matching Track 赛道战胜来自全球 1000 多支队伍,荣获季军。

    2022年 1月 9日
  • 2021图灵奖揭晓:高机能较量争论先驱、超算TOP500榜单创始人之一Jack Dongarra获奖

    他曾说过:未来的较量争论架构会是 CPU 和 GPU 的结合。

    2022年 3月 31日

发表回复

您的电子邮箱地址不会被公开。 必填项已用 * 标注