2007年图灵奖--克拉克、埃默生、希法凯斯简介

大家好，我是执念斩长河。今天讲述2007年图灵奖获得者克拉克、埃默生、希法凯斯。其中克拉克与埃默生是师生，希法凯斯是法国学者。图灵奖奖励他们为计算机辅助验证技术做出贡献。读完本篇博文大家可以收获：

克拉克身上的导师风范
三人各自贡献
什么是计算机辅助验证技术

克拉克于1945年7月27日生于美国弗吉尼亚州的Newport News。克拉克1967年在弗吉尼亚大学取得数学学士学位。第二年在杜克大学取得数学硕士学位，之后他专至康乃尔大学，于1974与1976年分别取得硕士与博士学位。
      埃默生于1976年在德州大学奥斯汀分校获得数学学士学位以后，转至哈佛大学师从克拉克。1951年获得博士学位。希法凯斯1946年12月26日出生在克里特岛的伊拉克利翁。从国立雅典理工大学毕业以后，获得奖学金至法国格勒诺布尔大学攻读博士学位。1974年获得博士学位。
      计算机辅助验证主要对象是计算机本身的硬件、软件和系统，说通俗点就是验证人类设计计算机各方面的正确性观察是否牢靠。为了验证正确性，埃默生发表了一篇论文《用分支时序逻辑设计和综合同步图》，论文提出这个方法既能验证又能验证硬件。这个方法：首先，为要验证的对象建立一个抽象模型，其形式化规约用时序逻辑表达。其次，他们提出了一种模型，可以确定该硬件或软件的设计是否符合相应的规约；若不符合，则给出一个反例，可以指出问题的根源在哪里。
其中规约、时序逻辑：
1996年图灵奖–阿米尔·伯努利简介
      这些发现只是在论文上，如果设计成软件进行商用又需要一段时间。1982年在论文写完过去的一年后，师生两人开发出“模型检验器”。好像跟希法凯斯没一点事情，错，同年他在法国也开发出类似的检验器。不过在对检验器优化是克拉克他们做的。使用了“二叉判定图”，一种用图形表示编码。大家可以认为很强的东西。
      克拉克做为一代导师从开门弟子埃默生到最近的弟子达到70多位。一次参加国际嵌入式会议时，精心制作幻灯片讲解弟子们的成就，并说：“我把我的成功归功于所有这些人。我所做的常常只是把他们指引到正确的方向并且坚持下去”。

2007年图灵奖--克拉克、埃默生、希法凯斯简介相关推荐

哀悼！2007年图灵奖得主Edmund Clarke因感染新冠逝世
转载自:AI科技评论最新消息,当地时间12月23日,2007年图灵奖得主Edmund M. Clarke(爱德蒙·克拉克)因感染新冠肺炎不幸去世. 其子James S. Clarke随后发推文缅怀父 ...
1975年图灵奖-赫伯特·西蒙和艾伦·纽厄尔简介
大家好,我是执念斩长河.今天要讲述的是1975年图灵奖两位获得者–赫伯特·西蒙和艾伦·纽厄尔.前者也曾获得诺贝尔经济学奖.读完本文大家可以收获的是: 西蒙得完诺贝尔再得图灵纽厄尔开创启发式程序逻辑理 ...
文学见识(含图灵奖历届指引)--目录
手动点击,无须翻阅:) 64.2020年图灵奖Jeffrey David Ullman和Alfred Vaino Aho简介 63.2019年图灵奖Edwin E. Catmull和Patrick M ...
2007图灵奖得主离开了：模型检测先驱Edmund Clarke因新冠逝世
视学算法报道作者:蛋酱.张倩 2020 还能更糟糕吗? 12 月 23 日,英特尔量子硬件研究组总监 James S. Clarke 发文表示,他的父亲.2007 年图灵奖得主 Edmund M. ...
2018年图灵奖--约书亚·本吉奥、杰弗里·埃弗里斯特·辛顿和Yann LeCun简介
大家好,我是执念斩长河.今天讲述的是2018年图灵奖获得者约书亚·本吉奥(Yoshua Bengio).杰弗里·埃弗里斯特·辛顿(Geoffrey Hinton)和Yann LeCun.图灵奖奖励他们 ...
【GPT-4】立即停止训练比 GPT-4 更强的模型，至少六个月！马斯克、图灵奖得主等数千 AI 专家紧急呼吁
毋庸置疑,ChatGPT.GPT-4 引领了 AI 新时代的到来,但这种让很多环节都可以实现自动化流程的工具也让人颇为恐慌. 据路透社报道,包括图灵奖得主 Yoshua Bengio.伯克利计算机科学 ...
历届图灵奖得主(1990-2022)
Robin Milner 1991年图灵奖得主贡献领域: LCF.ML编程语言.并发理论(CCS) 中文一般译作"罗宾·米尔纳", 1934年1月13日-2010年3月20日生 ...
专访图灵奖得主：完全自动驾驶是计算机接近人类智能的一大步
约瑟夫·斯发基斯(Joseph Sifakis) "我们什么时候会有完全自动驾驶的汽车?这将会是计算机向着接近人类智能所迈进的一大步."10月29日,2007年度图灵奖得主.国际嵌 ...
巨星陨落！图灵奖得主Edmund Clarke感染新冠逝世！
点击机器学习算法与Python学习 ,选择加星标精彩内容不迷路新智元报道当地时间12月22日,2007年图灵奖得主爱德蒙·克拉克(Edmund M. Clarke)因感染新冠肺炎不幸去世,享年 ...

2007年图灵奖--克拉克、埃默生、希法凯斯简介

2007年图灵奖--克拉克、埃默生、希法凯斯简介相关推荐

最新文章

热门文章