爱德蒙·克拉克(Edmund Clarke)简介
爱德蒙·克拉克(born July 27, 1945),1967年Clarke从美国南部的弗吉尼亚大学获得了其数学的学士学位,然后1968年从杜克大学完成了其数学的硕士学位的学业。9年之后的1976年,从康奈尔大学计算机系获得其博士学位。然后,Clarke在杜克大学任教两年。1978年,加入了哈佛大学并担任助理教授一职。1982年,Clarke离开哈佛加入了卡内基梅隆大学计算机系,并在1989年被评为全职终身教授一职。
Clarke一直专注于软硬件系统的验证和自动理论证明方面的研究工作。在他的博士论文中,其工作之一就是证明的在一些程序语言的控制逻辑中没有一个完善的Hoare理论证明系统。
1981年,他与自己的博士生Allen Emerson首次提出了模型检查的想法并用在自动机并发系统的验证研究上。成为形式逻辑研究方面模型检查的开创者之一。
Email: Edmund.Clarke@cs.cmu.edu
三位科学家获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年的图灵奖选择了模型检测技术编辑本段回目录
2007年图灵奖授予了在模型检测技术领域的奠基性贡献的科学家:Edmund M. Clarke、E Allen Emerson和Joseph Sifakis三位科学家。
什么是模型检测技术呢? 看看wikipedia 上的定义吧:
Model checking is the process of checking whether a given structure is a model of a given logical formula. The concept is general and applies to all kinds of logics and suitable structures. A simple model-checking problem is testing whether a given formula in the propositional logic is satisfied by a given structure.
简单的说:是一套用于判断硬件和软件设计的理论模型是否满足规范的方法。这可真是个抽象的描述,看起来似乎离我们很遥远,遥远的只有像英特尔研究中心副总 裁Andrew Chien才能对模型检测技术用一句话来评价:“英特尔和整个计算机工业都从他们的贡献中直接获益”。
那模型检测技术是不是离程序员也很遥远呢?图灵奖作为计算机界诺贝尔奖,如果把奖项颁给一个离程序员很遥远的技术,还真说不过去。
带着这个疑问,我浏览了wikipedia上长长的一窜模型检测技术的项目,还好不出所料,找到了下面几个项目:
1、Java Pathfinder :是一个用来认证java执行字节代码的系统。类似一个java虚拟机用来检测软件运行状态的验证系统。
2、Mono Model Checker :跑在mono 开源的.net平台上。用来自动侦查 CIL 字节码错误的程序。目前的版本支持CIL的死锁 deadlocks 和 断言冲突 assertion violation 。
3、对于c++ 感兴趣的人还可以看看这两个项目:
State Exploring Assembly Model Checker , Bounded Model Checking for ANSI-C 。
举个例子吧,在开发中,利用测试库junit 和 dotunit 写测试代码已经逐渐普及开了,比如下面这段:
public void testToppingsOnNewPizza(){ Pizza pizza = new Pizza(); List toppings = pizza.getToppings(); assert( (toppings.size()==0) );}
注意上面加黑的这句: assert( (toppings.size()==0) ); 。
这段代码我们用来检测:pizza.getToppings() 的大小是否为0。那么模型检测和上面的测试代码有什么不同呢?
不同点在于:现在的测试库用来判断结果 , 而模型检测用来判断过程(逻辑)是否符合要求。
我们常说,不但要关注结果,更要关注过程。模型检测就是对过程的关注。
无疑,现在写程序的时候,模型检测的过程,是由广大程序员完成的。如果这个过程可以由机器完成的话?那不是就是实现了自动编程吗?据说word的创始人开发者正在干这样的事儿... ,不知道这个老头有生之年能不能实现他的理想。
当然,我也相信在更高级的人工智能技术中,模型检测技术会大展拳脚。
2007年图灵奖获得者Edmund Clarke更多资料编辑本段回目录
Edmund Clarke(07/27/1945–)
图灵奖获得时间: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.
(授予Edmund Clarke图灵奖以表彰其)对目前在硬件和软件领域被广泛使用的模型检查发展成为一个重要的,高效的验证技术所做出的杰出贡献。
关于模型检查理论,可参阅美国卡内基梅隆(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(图灵奖演讲文章):
Edmund Clarke简介:
1967年Clarke从美国南部的弗吉尼亚大学获得了其数学的学士学位,然后1968年从杜克大学完成了其数学的硕士学位的学业。9年之后的1976年,从康奈尔大学计算机系获得其博士学位。然后,Clarke在杜克大学任教两年。1978年,加入了哈佛大学并担任助理教授一职。1982年,Clarke离开哈佛加入了卡内基梅隆大学计算机系,并在1989年被评为全职终身教授一职。
Clarke一直专注于软硬件系统的验证和自动理论证明方面的研究工作。在他的博士论文中,其工作之一就是证明的在一些程序语言的控制逻辑中没有一个完善的Hoare理论证明系统。
1981年,他与自己的博士生Allen Emerson首次提出了模型检查的想法并用在自动机并发系统的验证研究上。成为形式逻辑研究方面模型检查的开创者之一。
Edmund Clarke的wiki: http://en.wikipedia.org/wiki/Edmund_M._Clarke
Edmund Clarke在CMU主页:http://www.cs.cmu.edu/~emc/