Solidot 登录
[ 创建一个新帐号 ]
2007年图灵奖宣布
美国计算机协会宣布了2007年图灵奖获得者：Edmund M. Clarke，Allen Emerson和Joseph Sifakis在开发自动化方法检测计算机硬件和软件中的设计错误上的贡献而授予此计算机行业的最重要奖项。
模型检测（Model Checking）是一类“验证”，分析设计背后的逻辑，就像数学家用证明来判断一个定理是否正确。模型检测并非是胡乱的检查，它要考虑硬件和软件设计的每一种可能情况，判断它是否与设计者的规范一致。1981年，哈佛大学的Clarke和Emerson提出了模型检测的最初理念。他们开发了一套理论方法判断硬件和软件设计的理论模型是否满足正式规范，赋予一个时序逻辑规则，描述事情发展可能性的一个符号。此外，当系统检测失败，它还能确定源代码中的问题存在位置。目前已经许多模型检测系统在使用，Clarke在1982年实现了第一个模型检测器。
声明:
下面的评论属于其发表者所有，不代表本站的观点和立场，我们不负责他们说什么。
获奖年份
(得分:1)( http://talk.blogbus.com/ | 最新日志: 2008年1月31日 19时27分 星期四 )