《2007年图灵奖获得者》由会员分享，可在线阅读，更多相关《2007年图灵奖获得者（3页珍藏版）》请在金锄头文库上搜索。
1、20072007 年图灵奖获得者：年图灵奖获得者：EdmundEdmund M.M. ClarkeClarke，AllenAllen EmersonEmerson 和和 JosephJoseph SifakisSifakis美国计算机协会 2008 年 2 月 4 日宣布了 2007 年图灵奖获得者：Edmund M. Clarke(艾 德蒙德克拉克)，Allen Emerson(艾伦埃莫森)和 Joseph Sifakis(约瑟夫西法基斯) 三位科学家，表彰他们开发模型检测技术，并使之成为一个广泛应用在硬件和软件工业中 非常有效的算法验证技术所做的奠基性贡献。 背景知识背景知识：模型检查及其
2、历史 模型检测（Model-Checking，也译为模型检验，仿真术语里称为模型校验）是一类 “验证” ，分析设计背后的逻辑，就像数学家用证明来判断一个定理是否正确。其本质上是 用严密的数学方法来验证设计是否满足预设的需求，从而自动化地发现设计中的错误。按 Wikipedia 的定义，它是一种检查某一给定模型是否满足某一逻辑规则的方法。其中一种 重要的方法，就是通过算法来验证形式化系统，具体方法是验证由硬件或者软件设计导出 的模型是否满足通常用模态逻辑规则表示的形式化规范。 在硬件业，包括半导体业和嵌入式系统中，模型检查已经成为一项非常关键的主流技 术。 要知道，在硬件行业，如果设计有问题，一
3、旦投产，损失就太大了。正因为这样，图灵奖 赞助方之一 Intel 对三位获奖者的祝贺可以说是充满了感激之情。此外，在通信协议、安 全算法的设计方面，模型检查也发挥了关键作用。 但是，软件业对模型检查的重视似乎很不够。一线的软件开发人员可能都对它比较陌 生，感觉比较学院化。当然，由于存在可计算性导致的缺陷，以及软件本身的复杂性，模 型检查是不可能完全解决软件设计中的 bug 的。但是，软件业对这种方法的忽视，是否也 是软件总体质量不如硬件，或者说低级错误更多的一个原因呢？ 总之，模型检查在工业检测方面有诸多应用：如芯片检测、通信协议、外部设备主控 软件、嵌入式系统（如在飞机、火车、火箭、卫星或移
4、动电话）以及安全算法等。 历史背景：关于模型检查的最初论文，是 1981 年由 Clarke 和 Emerson 在哈佛大学， Sifakis 和 J.P. Queille 在法国，分别独立撰写的。1982 年，Clarke 还实现了第一个模 型检查程序。但由于状态爆炸问题，最初的模型检查只能应用于很小规模的设计，从而无 法走出学院。 1987 年，Clarke 的博士生 Kenneth McMillan 发现，在另一位 CMU 教授 Randal E. Bryant 运用二叉决策图（BDD，binary decision diagram）表示符号信息的工作基础上， 可以发明一种新的模型检查实
5、现方法，也就是所谓符号模型检查（Symbolic Model Checking） ，将突破该方法的复杂度限制，从而广泛开始应用于工业界，尤其是半导体制造 业。为此，Bryant, Clarke,Emerson 和 McMillan 获得了 1998 年 ACM Paris Kanellakis 奖。而 Sifakis 则与 Thomas A. Henzinger、Sergio Yovine 将模型检查方法应用于实时系 统的验证。 获奖者获奖者 1 1：EdmundEdmund M.M. ClarkeClarke(艾德蒙德克拉克) Clarke 是卡耐基梅隆大学（CMU）的教授，曾任 Forma
6、l 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 Univer
7、sity Press（此书有中译本） (2)Model Checking，Edmund M. Clarke, Orna Grumberg, and Doron Peled ，MIT Press 获奖者获奖者 2 2：E.E. AllenAllen EmersonEmerson(艾伦埃莫森) Emerson 是得克萨斯大学奥斯汀分校教授，曾任 ACM Transactions on Computational Logic, Formal Aspects of Computing,和 Formal Methods in Systems Design 等杂志的编委。他拥有得克萨斯大学奥斯汀分校数学学
8、 士和硕士学位，哈佛大学应用数学博士学位。他的主页透露，自己之所以走 上形式化验证的道路，是受了 1970 年代中期图灵奖得主 Tony Hoare 的一篇 CACM 论文“Proof of Program:Find”的启发。他位列 CiteSeer 引用次数 最多的前 1%计算机科学家。 获奖者获奖者 3 3：JosephJoseph SifakisSifakis(约瑟夫西法基斯) Joseph Sifakis 是位于法国格勒诺布尔(Grenoble)的以嵌入式系统 著称世界的研究中心 Verimag 实验室（UJF/CNRS/INPG）的创始人。现在 是法国国家科研中心（Centre Na
9、tional de la Recherche Scientifique，简称为 CNRS）的研究总监和 CARNOT Institute on Intelligent Software and Systems in Grenoble 的负责人。他在雅典 技术大学获得电机工程博士学位，在 Grenoble(格勒诺布尔)大学获得计算机科学博士学位。 他是第一个获得图灵奖的法国人。 由于在将模型检查方法应用于实时系统的验证方面的工作而使 Joseph Sifaki 在国际 上获得声誉。他是广泛应用于工业界的“模型检测”技术的发明者。Joseph Sifakis 的研 究工作具有决定性意义并且引导出了
10、新的软件规范的创建、新的检测算法以及杰出的理论 结果。这项技术今天被应用于集成电路工业中以便设计复杂的系统并能够使其保证符合预 设的规范。模型检查在嵌入式处理器和关键系统方面的产业影响在未来的几年里将会更加 显著。20072007 TuringTuring AwardAward WinnersWinners AnnouncedAnnouncedFor their groundbreaking work on Model CheckingEdmundEdmund M.M. ClarkeClarke, E.E. AllenAllen EmersonEmerson, and JosephJoseph
11、 SifakisSifakis 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 ModelModel CheckingChecking, is the most widely used technique for detecting and diagnosing errors in complex hardwar
12、e 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, present
13、ed 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 unde
14、rlying 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 i
15、dea 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 t
16、he 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 g
