2007年图灵奖获得者.doc

2007年图灵奖获得者： Edmund M. Clarke，Allen Emerson和Joseph Sifakis 美国计算机协会2008年2月4日宣布了2007年图灵奖获得者：Edmund M. Clarke(艾德蒙德·克拉克)，Allen Emerson(艾伦·埃莫森)和Joseph Sifakis(约瑟夫·西法基斯)三位科学家，表彰他们开发模型检测技术，并使之成为一个广泛应用在硬件和软件工业中非常有效的算法验证技术所做的奠基性贡献。模型检查在工业检测方面有诸多应用：如芯片检测、通信协议、外部设备主控软件、嵌入式系统（如在飞机、火车、火箭、卫星或移动电话）以及安全算法等。获奖者1：Edmund M. Clarke(艾德蒙德·克拉克) Clarke是卡耐基·梅隆大学（CMU）的教授，曾任 Formal Methods in Systems Design 杂志主编。曾任荣获2004年IEEE Harry M. Goode 纪念奖。ACM和 IEEE 计算机学会会士，2005年当选美国工程院院士。本科毕业于弗吉尼亚大学，硕士在杜克大学，均为数学专业，然后在康奈尔大学获得计算机博士学位。曾任教杜克大学和哈佛大学。他在CMU的模型检查课程。主要教材是： (1)Logic in Computer Science: Modeling and reasoning about systems Michael R A Huth and Mark D Ryan Cambridge University Press（此书有中译本） (2)Model Checking，Edmund M. Clarke, Orna Grumberg, and Doron Peled ，MIT Press 获奖者2：E. Allen 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%计算机科学家。 获奖者3：Joseph Sifakis(约瑟夫·西法基斯) Joseph Sifakis 是位于法国格勒诺布尔以嵌入式系统著称世界的研究中心Verimag实验室（UJF/CNRS/INPG）的创始人。法国国家科研中心（CNRS）的研究总监格勒诺布尔是奖的法国人。由于在将模型检查方法应用于实时系统的验证方面的工作而使Joseph Sifaki在国际上获得声誉。他是广泛应用于工业界的“模型检”技术的发明者。Joseph Sifakis的研究工作具有决定性意义并且引导出了新的软件规范的创建、新的检测算法以及杰出的理论结果。这项技术今天被应用于集成电路工业中以便设计复杂的系统并能够使其保证符合预设的规范。模型检查在嵌入式处理器和关键系统方面的产业影响在未来的几年里将会更加显著。2007 Turing Award Winners Announced For their groundbreaking work on Model Checking Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis are the recipients of the 2007 A.M. Turing Award for their work on an automated method for finding design errors in computer hardware and software. The method, called Model Checking, is the most widely used technique for detecting and diagnosing errors in complex hardware and software design. It has helped to improve the reliability of complex computer chips, systems and networks. Clarke, a professor at Carnegie Mellon University,Emerson,of the Unive