艾伦·爱默生(Ernest Allen Emerson),是Edmund Clarke在哈佛大学的博士生。
著名的“模型检测”的论文就是Emerson与导师Clarke合作的。Emerson是从德州奥斯丁分校获得的其数学本科学位,并从哈佛大学应用数学系获得其博士学位。Emerson是得克萨斯大学奥斯汀分校教授,曾任 ACM Transactions on Computational Logic, Formal Aspects of Computing, 和 Formal Methods in Systems Design 等杂志的编委。他拥有得克萨斯大学奥斯汀分校数学学士和硕士学位,哈佛大学应用数学学位。
他的主页透露,自己之所以走上形式化验证的道路,是受了1970年代中期图灵奖得主Tony Hoare的一篇CACM 论文"Proof of Program: Find"的启发。他位列CiteSeer引用次数最多的前1%计算机科学家。
三位科学家获2007年度图灵奖编辑本段回目录
美国计算机协会(ACM)近日公布了2007年度图灵奖(Turing Award)的评选结果,本年度图灵奖授予Edmund M. Clarke、E Allen Emerson和Joseph Sifakis三位科学家,表彰他们开发模型检测技术,并使之成为一个广泛应用在硬件和软件工业中非常有效的算法验证技术所做的奠基性贡献。
1981年在美国工作的Edmund Clarke和Allen Emerson以及在法国的Sifakis分别提出了模型检测(Model Checking)的最初概念,并且他们开发了一套用于判断硬件和软件设计的理论模型是否满足规范的方法,此外,当系统检测失败时,还能利用它确定代码中问题存在的位置。
英特尔研究中心副总裁Andrew Chien说:“英特尔和整个计算机工业都从他们的贡献中直接获益”。Google的高级工程副总裁Alan Eustace说:“Google像其他同时代的技术公司一样,很大一部分成功都来自于先驱们的研究贡献”。
图灵奖由美国计算机协会于1966年设立,专门奖励那些对计算机事业做出重要贡献的个人,其名称取自计算机科学先驱,英国科学家阿兰·图灵。获奖者的贡献必须在计算机领域具有持久而重大的影响。
图灵奖有“计算机界诺贝尔奖”之称,对获奖者要求极高,评奖程序亦极严格,目前由英特尔和Google公司赞助,奖金为25万美元。
目前获此殊荣的华人科学家仅姚期智一人。
2007年图灵奖获得者Allen Emerson更多资料编辑本段回目录
E Allen Emerson 图灵奖获得时间:2007年。 第42位图灵奖(2007年)获得者。
图灵奖引用(Turing Award Citation) :
For his role in developing Model-Checking into a highly effective verification technology, widely adopted in the hardware and software industries.
(授予Allen Emerson图灵奖以表彰其)对目前在硬件和软件领域被广泛使用的模型检查发展成为一个重要的,高效的验证技术所做出的杰出贡献。
关于模型检查理论,可参阅美国卡内基梅隆(CMU)计算机系的模型检查(Model Check)实验室:
http://www.cs.cmu.edu/~modelcheck/
理论而言,模型检查属于形式方法(Formal Methods)研究的一个分支 。关于形式理论,可以参阅:http://en.wikipedia.org/wiki/Formal_methods
另外,也可参阅:
http://en.wikipedia.org/wiki/Model_checking
Turing Award Lecture(图灵奖演讲文章):
Allen Emerson简介:
Allen Emerson是Edmund Clarke在哈佛大学的博士生。著名的“模型检测”的论文就是Emerson与导师Clarke合作的。Emerson是从德州奥斯丁分校获得的其数学本科学位,并从哈佛大学应用数学系获得其博士学位。
关于Emerson的更多信息可参见其在德州大学奥斯丁分校计算机系的主页: