为什么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的创始人开发者正在干这样的事儿... ,不知道这个老头有生之年能不能实现他的理想。
当然,我也相信在更高级的
人工智能技术中,模型检测技术会大展拳脚。
又是个遥远的事情,洗洗睡吧。
分享到:
相关推荐
图灵奖 图灵奖 图灵奖 图灵奖 图灵奖 图灵奖图灵奖图灵奖图灵奖
通过从1966年开始的图灵奖,逐年介绍当年的图灵奖获得者。到目前为止,是图 灵奖的第一个 40年(1966–2005)。总共有 50位杰出的科学家获得了此荣誉。到现 在为止(2008年 2月 8日)近 2年过去了。新的 4位图灵奖获得...
1966-2016年图灵奖获得者 2008-2016年图灵奖获得者详细资料
图灵奖是计算机界的最高奖项,由ACM发起,本资料收录了66-94年图灵奖获得者在ACM大会上的讲话。(共四个分卷)
做大事,成大业 YOU AND YOUR RESEARCH - RICHARD HAMMING,前贝尔实验室著名计算机科学家,1968年因其在“数值方法,自动编码系统,错误检测和纠错码”方面的贡献获得图灵奖。
图灵奖是计算机界的最高奖项,由ACM发起,本资料收录了66-94年图灵奖获得者在ACM大会上的讲话。(共四个分卷)
INVENTOR OF WORLD WIDE WEB RECEIVES ACM A.M. TURING AWARD Sir Tim Berners-Lee Designed Integrated Architecture and Technologies that Underpin the Web
图灵奖是计算机界的最高奖项,由ACM发起,本资料收录了66-94年图灵奖获得者在ACM大会上的讲话。(共四个分卷)
1966--2005图灵奖获得者国籍、学历、年龄分布
此资源整理了历届图灵奖得主,份额,年份,获奖介绍等字段,压缩包内包含json形式和csv表格excel格式。
图灵奖是计算机界的最高奖项,由ACM发起,本资料收录了66-94年图灵奖获得者在ACM大会上的讲话。(共四个分卷)
图灵奖演讲集:前20年(1966-1985).pdf
图灵奖大师的讲座,很难得的,他写了好多算法,在计算机领域作出杰出的贡献,看了之后会受益匪浅的。。。
20世纪 几届 ACM图灵奖
三位在数据库领域作出杰出贡献的图灵奖获得者
数据库领域图灵奖获得者信息介绍 Michael Stonebraker 他比较新的观点认为,数据库领域可以有很多赢家,“将有3到5个,甚至 6个非常不同的数据库系统架构成为赢家,而在每一类下都会有2到3个成 功的供应商。...
计算的美丽-图灵奖获得者2 电子书 pdf
图灵奖得主Judea Pearl:机器学习无法成为强AI基 础,突破口在“因果革命”
图灵机模型与现代计算机演化,
图灵奖,全称为A.M.图灵奖(ACM A.M Turing Award),是由美国计算机协会(ACM)于1966年设立的奖项。这一奖项以计算机科学的先驱、英国科学家艾伦·麦席森·图灵(Alan M. Turing)的名字命名,旨在奖励那些对...