2007年图灵奖获得者.doc

2007年图灵奖获得者：Edmund M. Clarke，Allen Emerson和Joseph Sifakis美国计算机协会2008年2月4日宣布了2007年图灵奖获得者：Edmund M. Clarke(艾德蒙德克拉克)，Allen Emerson(艾伦埃莫森)和Joseph Sifakis(约瑟夫西法基斯)三位科学家，表彰他们开发模型检测技术，并使之成为一个广泛应用在硬件和软件工业中非常有效的算法验证技术所做的奠基性贡献。背景知识：模型检查及其历史模型检测（Model-Checking，也译为模型检验，仿真术语里称为模型校验）是一类“验证”，分析设计背后的逻辑，就像数学家用证明来判断一个定理是否正确。其本质上是用严密的数学方法来验证设计是否满足预设的需求，从而自动化地发现设计中的错误。按Wikipedia的定义，它是一种检查某一给定模型是否满足某一逻辑规则的方法。其中一种重要的方法，就是通过算法来验证形式化系统，具体方法是验证由硬件或者软件设计导出的模型是否满足通常用模态逻辑规则表示的形式化规范。在硬件业，包括半导体业和嵌入式系统中，模型检查已经成为一项非常关键的主流技术。要知道，在硬件行业，如果设计有问题，一旦投产，损失就太大了。正因为这样，图灵奖赞助方之一Intel对三位获奖者的祝贺可以说是充满了感激之情。此外，在通信协议、安全算法的设计方面，模型检查也发挥了关键作用。但是，软件业对模型检查的重视似乎很不够。一线的软件开发人员可能都对它比较陌生，感觉比较学院化。当然，由于存在可计算性导致的缺陷，以及软件本身的复杂性，模型检查是不可能完全解决软件设计中的bug的。但是，软件业对这种方法的忽视，是否也是软件总体质量不如硬件，或者说低级错误更多的一个原因呢？总之，模型检查在工业检测方面有诸多应用：如芯片检测、通信协议、外部设备主控软件、嵌入式系统（如在飞机、火车、火箭、卫星或移动电话）以及安全算法等。历史背景：关于模型检查的最初论文，是1981年由Clarke和Emerson在哈佛大学，Sifakis和J.P. Queille在法国，分别独立撰写的。1982年，Clarke还实现了第一个模型检查程序。但由于状态爆炸问题，最初的模型检查只能应用于很小规模的设计，从而无法走出学院。1987年，Clarke的博士生Kenneth McMillan发现，在另一位CMU教授Randal E. Bryant运用二叉决策图（BDD，binary decision diagram）表示符号信息的工作基础上，可以发明一种新的模型检查实现方法，也就是所谓符号模型检查（Symbolic Model Checking），将突破该方法的复杂度限制，从而广泛开始应用于工业界，尤其是半导体制造业。为此，Bryant, Clarke,Emerson和McMillan获得了1998年ACM Paris Kanellakis奖。而Sifakis则与Thomas A. Henzinger、Sergio Yovine将模型检查方法应用于实时系统的验证。获奖者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 是位于法国格勒诺布尔(Grenoble)的以嵌入式系统著称世界的研究中心Verimag实验室（UJF/CNRS/INPG）的创始人。现在是法国国家科研中心（Centre National de la Recherche Scientifique，简称为CNRS）的研究总监和CARNOT Institute on Intelligent Software and Systems in Grenoble的负责人。他在雅典技术大学获得电机工程博士学位，在Grenoble(格勒诺布尔)大学获得计算机科学博士学位。他是第一个获得图灵奖的法国人。由于在将模型检查方法应用于实时系统的验证方面的工作而使Joseph Sifaki在国际上获得声誉。他是广泛应用于工业界的“模型检测”技术的发明者。Joseph Sifakis的研究工作具有决定性意义并且引导出了新的软件规范的创建、新的检测算法以及杰出的理论结果。这项技术今天被应用于集成电路工业中以便设计复杂的系统并能够使其保证符合预设的规范。模型检查在嵌入式处理器和关键系统方面的产业影响在未来的几年里将会更加显著。2007 Turing Award Winners AnnouncedFor their groundbreaking work on Model CheckingEdmund 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 University of Texas,Austin, and Joseph Sifakis of the University of Grenoble,will share $250,000. The Turing Award, presented annually by the Association for Computing Machinery, is considered to be the most prestigious award in computing. Often referred to as the Nobel Prize of computing, it is named for British mathematician Alan M. TuringModel Checking is a type of formal verification that analyzes the logic underlying a design, much as a mathematician uses a proof to determine that a theorem is correct. Far from hit or miss, Model Checking considers every possible state of a hardware or software design and determines if it is consistent with the designers specifications. Clarke and Emerson originated the idea of Model Checking at Harvard in 1981. They developed a theoretical technique for determining whether an abstract model of a hardware or software design satisfies a formal specification, given as a formula in Temporal Logic, a notation for describing possible sequences of events. Moreover, when the system fails the specification, it could identify a counterexample to show the source of the problem. Numerous model checking systems have been implemented, such as Spin at Bell Labs.Clarke implemented the first Model Checker in 1982. It could analyze all the possible states of a given circuit, but was limited to relatively small designs - much smaller than the systems being built by computer manufacturers. In 1987, Clarkes graduate student, Kenneth McMillan, realized that he could implement Model Checking by a series of operations on binary decision diagrams (BDDs), a method of representing symbolic information that had recently been developed by another Carnegie Mellon computer science professor, Randal E. Bryant. This new system, called Symbolic Model Checking, was able to analyze billions of billions of states, making it relevant to commercial computer design problems and l