美国卡内基梅隆大学计算机系教授、中国科学院“爱因斯坦讲席教授”、图灵奖得主EdmundClarke于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 BDDs”的讲座。Clarke教授深入浅出地介绍了符号化模型检查的由来与基本算法原理，还兴致勃勃地讲述了在1992年他与他的学生们采用该模型检查算法检测到一个缓存一致性协议存在缺陷的故事，这一协议来自一个当时已经公布四年之久的工业标准协议（IEEE FutureBus+ Standard）。这是第一个采用形式化方法在IEEE标准中找到错误的应用案例，展现了模型检查方法在工业硬件设计领域中的应用前景。10月23日上午，Clarke教授为研究中心师生带来了第二场专场讲座，题目为“Bounded Model Checking with SAT/SMT”。Clarke教授在这个讲座中重点讲述了他在模型检查方法中取得的一个重大突破——目前已在工业界广泛采用的基于SAT工具的限界模型检查方法。研究中心的师生表示通过这个内容详实的讲座学习到了模型检查最前沿的研究成果与工业应用，收获颇丰。
随后的几天里，Clarke教授与研究院的师生进行了面对面的深入交流，并听取了中科大-耶鲁高可信软件联合研究中心、嵌入式系统实验室等团队的工作介绍。Clarke教授对苏州研究院各团队的研究课题表示出了极大的兴趣，并提出了宝贵意见。
（计算机学院、苏州研究院）
