简介

研究工作

成就

获奖

相关资料

简介

爱德蒙·克拉克（Edmund Clarke）(born July 27, 1945)，1967年Clarke从美国南部的弗吉尼亚大学获得了其数学的学士学位，然后1968年从杜克大学完成了其数学的硕士学位的学业。9年之后的1976年，从康奈尔大学计算机系获得其博士学位。然后，Clarke在杜克大学任教两年。1978年，加入了哈佛大学并担任助理教授一职。1982年，Clarke离开哈佛加入了卡内基梅隆大学计算机系，并在1989年被评为全职终身教授一职。

研究工作

Clarke一直专注于软硬件系统的验证和自动理论证明方面的研究工作。在他的博士论文中，其工作之一就是证明的在一些程序语言的控制逻辑中没有一个完善的Hoare理论证明系统。

成就

1981年，他与自己的博士生Allen Emerson首次提出了模型检查的想法并用在自动机并发系统的验证研究上。成为形式逻辑研究方面模型检查的开创者之一。

获奖

2007年度图灵奖授予Edmund M. Clarke、E Allen Emerson和Joseph Sifakis三位科学家，表彰他们开发模型检测技术，并使之成为一个广泛应用在硬件和软件工业中非常有效的算法验证技术所做的奠基性贡献。

相关资料

图灵奖由美国计算机协会于1966年设立，专门奖励那些对计算机事业做出重要贡献的个人，其名称取自计算机科学先驱，英国科学家阿兰?图灵。获奖者的贡献必须在计算机领域具有持久而重大的影响。

图灵奖有“计算机界诺贝尔奖”之称，对获奖者要求极高，评奖程序亦极严格，目前由英特尔和Google公司赞助，奖金为25万美元。

目前获此殊荣的华人科学家仅姚期智一人。