Languages

中科院“爱因斯坦讲席教授”、图灵奖得主Edmund Clarke教授访问中科大-耶鲁高可信软 件联合研究中心

   美国卡内基梅隆大学计算机系教授、中国科学院“爱因斯坦讲席教授”、图灵奖得主
Edmund Clarke于2013年10月20日至27日对中科大苏州研究院和中科大--耶鲁高
可信软件联合研究中心进行了为期8天的学术访问与交流。
   
       Edmund Clarke教授是形式化验证领域中模型检查(Model Checking)技术的
创始人之一,他是美国计算机学会(ACM)与美国电气电子工程师学会(IEEE)院
士,同时也是美国国家科学院和工程院院士。Clarke教授于2007年和另外两位科学家
E.Allen Emerson和Joseph Sifakis一同分享了 “图灵奖”,以表彰他们对模型检查
理论与技术做出的奠基性贡献。目前模型检查技术已成为一个被广泛应用在硬件和软
件工业中非常有效的验证技术。
 
10月21日上午,Clarke教授为中科大苏州研究院的师生带来了题为“Model Checking
and the Curse of Dimensionality” 的精彩报告。Clarke教授在演讲中回顾了模型检查
理论技术的发展历程,分析了在过去20多年里面遇到的四个典型的难题,讲解了科研人
员如何解决这些难题并取得重大突破。
 
10月22日上午,Clarke教授针对中科大-耶鲁高可信软件联合研究中心的师生作了一个题为“Symbolic Model Checking with BD
Ds”的讲座。Clarke教授深入浅出地介绍了符号化模型检查的由来与基本算法原理,还兴致勃勃地讲述了在1992年他与他的学生
们采用该模型检查算法检测到一个缓存一致性协议存在缺陷的故事,这一协议来自一个当时已经公布四年之久的工业标准协议
(IEEE FutureBus+ Standard)。这是第一个采用形式化方法在IEEE标准中找到错误的应用案例,展现了模型检查方法在工
业硬件设计领域中的应用前景。10月23日上午,Clarke教授为研究中心师生带来了第二场专场讲座,题目为“Bounded Model
Checkingwith SAT/SMT”。Clarke教授在这个讲座中重点讲述了他在模型检查方法中取得的一个重大突破——目前已在工业界
广泛采用的基于SAT工具的限界模型检查方法。研究中心的师生表示通过这个内容详实的讲座学习到了模型检查最前沿的研究成
果与 工业应用,收获颇丰。

在10月21日、22日的下午,冯新宇教授向Clarke教授介绍了近几年来研究中心在并发程序验证理论、还有在操作系统内核验证理
论方面的取得的研究成果,研究中心的其他老师、博士后与研究生们也参与并展开了热烈的讨论。Clarke教授高度评价了研究中心
的研究成果,并对研究中心的研究课题表示出了极大的兴趣。在随后的几天中,Clarke教授继续与研究中心的师生进行了面对面的
深入交流,并对于研究中心的正在展开的研究课题提出了宝贵的意见。