2007年图灵奖揭晓

据ACM的官方消息，Edmund M. Clarke，Allen Emerson和Joseph Sifakis因为“在将模型检查发展为被硬件和软件业中所广泛采纳的高效验证技术上的贡献”（For his role in developing Model-Checking into a highly effective verification technology, widely adopted in the hardware and software industries）而荣获2007年的图灵奖。

而DDJ的报道则将三人的贡献称为“在发现计算机硬件和软件中设计错误的自动化方法方面的工作”（for their work on an automated method for finding design errors in computer hardware and software）。

背景知识：模型检查

模型检查（Model-Checking，也译为模型检验，仿真术语里称为模型校验）本质上是用严密的数学方法来验证设计是否满足预设的需求，从而自动化地发现设计中的错误。按Wikipedia的定义，它是一种检查某一给定模型是否满足某一逻辑规则的方法。其中一种重要的方法，就是通过算法来验证形式化系统，具体方法是验证由硬件或者软件设计导出的模型是否满足通常用模态逻辑规则表示的形式化规范。

在硬件业，包括半导体业和嵌入式系统中，模型检查已经成为一项非常关键的主流技术。 要知道，在硬件行业，如果设计有问题，一旦投产，损失就太大了。正因为这样，图灵奖赞助方之一Intel对三位获奖者的祝贺可以说是充满了感激之情。

此外，在通信协议、安全算法的设计方面，模型检查也发挥了关键作用。

但是，软件业对模型检查的重视似乎很不够。一线的软件开发人员可能都对它比较陌生，感觉比较学院化。当然，由于存在可计算性导致的缺陷，以及软件本身的复杂性，模型检查是不可能完全解决软件设计中的bug的。但是，软件业对这种方法的忽视，是否也是软件总体质量不如硬件，或者说低级错误更多的一个原因呢？

关于模型检查，一般软件工程教科书里会有一些章节介绍，embedded.com上有一篇很好的介绍性文章。

获奖者1：Edmund M. Clarke

Clarke是卡耐基梅隆大学（CMU）的教授，曾任 Formal Methods in Systems Design 杂志主编。曾任荣获2004年IEEE Harry M. Goode 纪念奖。ACM和 IEEE 计算机学会会士，2005年当选美国工程院院士。本科毕业于弗吉尼亚大学，硕士在杜克大学，均为数学专业，然后在康奈尔大学获得计算机博士学位。曾任教杜克大学和哈佛大学。

他在CMU的模型检查课程。主要教材是：

Logic in Computer Science: Modeling and reasoning about systems
Michael R A Huth and Mark D Ryan
Cambridge University Press（此书有中译本）

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

Sifakis是 位于法国Grenoble的顶尖嵌入式系统研究中心Verimag实验室的创始人。现在是Centre National de la Recherche Scientifique的研究总监和CARNOT Institute on Intelligent Software and Systems in Grenoble的负责人。他在雅典技术大学获得电机工程学位，在Grenoble大学获得计算机科学博士学位。

背景

关 于模型检查的最初论文，是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将模型检查方法应用于实时系统的验证。

八卦

图灵奖原来的奖金2002年开始由Intel独家赞助。由于Google的加入，有“计算机诺贝尔奖”之称的ACM 图灵奖奖金将由原来的10万美元，增加到25万美元。新奖金额的2007年图灵奖将在2008年春季揭晓。

【广告】图灵公司正是name after阿兰·图灵，公司的口号是“站在巨人肩上”。