计算的美丽–2007年图灵奖获得者Edmund Clarke

作者 | 2008-04-07 15:10 | 类型 人物评述, 计算的美丽 | Comments Off

Sina WeiboBaiduLinkedInQQGoogle+RedditEvernote分享




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/

Edmund Clarke照片:

(没有打分)

工具箱
本文链接 | | 打印此页 | Comments Off

雁过留声

Comments are closed.