中国科学院“爱因斯坦讲席教授”、图灵奖获得者Edmund M. Clarke教授来访
10月15日至18日，应计算机科学国家重点实验室邀请，中国科学院“爱因斯坦讲席教授”、2007年ACM图灵奖获得者美国卡内基梅隆大学Edmund M. Clarke教授到软件所进行访问交流，并分别作了三场学术报告。来自清华大学、北京大学、北京航空航天大学等院校的近百名老师和学生聆听了报告。
15日上午，Clarke教授作了题为Model Checking and the Curse of Dimensionality的报告。报告中，Clarke教授浅入深出地对模型检测技术进行了阐述。模型检测是一种自动验证技术，由Clarke、Emerson和Quielle、Sifakis分别在1981年独立提出，在过去三十年中对计算机科学的理论和实践都产生了重大的影响，取得了极大的成功，并在工业界得到了广泛的应用。
在讲到模型检测技术面临的挑战时，Clark教授介绍了近三十年来在解决状态空间爆炸问题方面所取得的几个里程碑式的进展。他还介绍了模型检测技术在软件、信息物理融合系统、生物信息学等领域的应用前景。
16日上午，在题为Symbolic Model Checking with Ordered Binary Decision Diagrams的报告中，Clarke教授介绍了其在符号模型检测方面的研究。他认为，符号模型检测技术是自动验证领域的重要贡献之一，而有序二叉判定图（OBDD）的唯一性是符号模型检测技术成功的关键。
17日上午，Clarke教授作了题为Bounded Model Checking with SAT/SMT的报告。报告主要讲述了其在限界模型检测方面的研究，并介绍了其团队在复杂混成系统验证方面的最新研究成果。报告中，Clarke教授还鼓励探索不同分析、验证技术（如定理证明、静态分析等）的有机结合。
三场报告内容精彩，激起了大家的浓厚兴趣。Clarke教授回答了听众提出的大量问题，并就组合验证、概率模型检测等学术问题进行了热烈的讨论。
15日下午和18日上午，Clarke教授还听取了实验室研究人员在符号模型检测、限界模型检测、混成系统验证、概率模型检测及假设—保证推理等方面的工作报告，并就相关技术细节进行了深入、细致地讨论，双方对促进未来合作研究都充满期待。
演讲人简介：
Clarke教授1967年在弗吉尼亚大学获得数学学士学位，1968年在杜克大学获得数学硕士学位，1976年在康奈尔大学获得计算机博士学位。然后，Clarke教授在杜克大学任教两年，于1978年加入哈佛大学并担任助理教授。1982年，加入卡内基梅隆大学计算机系。
Clarke教授曾获IEEE Harry M. Goode纪念奖（2004年）， ACM图灵奖（2007年），Herbrand奖（2008年）。
Clarke教授2005年当选美国工程院院士，2011年当选美国艺术和科学院院士。他是ACM和IEEE Fellow。
报告下载：