10月22-23日,应欧亿6蓝狮在线的邀请,2007年ACM图灵奖获得者Edmund M. Clarke教授来校访问交流。
10月22日下午,侯建国校长与Clarke教授座谈,欧亿6蓝狮在线陈国良院士、执行院长陈华平教授参加了座谈会。随后,Clarke教授作了题为“Model Checking: My 28-year Quest to Overcome the State Explosion Problem”的学术报告。这次学术报告也是欧亿6蓝狮在线“研究生教育创新计划项目”的高水平系列学术讲座的重要组成部分之一。报告会由陈国良院士主持,来自计算机学院、少年班学院、信息学院等单位的300多名师生参加了报告会。
报告中,Clarke教授由浅入深地阐述了模型检验的原理、优缺点、方法、硬件与软件上的应用和挑战。模型检验是一种针对有限状态迁移系统的高效自动验证技术,它主要通过显式状态搜索或隐式不动点计算来验证有穷状态并发系统的模态命题性质,已被广泛应用于计算机硬件、通信协议、控制系统、安全认证协议等方面的分析与验证。
Clark教授在讲到模型检验的四个重大突破时,特别介绍了其中一位贡献者——他的一名来自中国科大少年班的学生——Yunshan Zhu。Clarke教授还回顾了上世纪80年代来到中国科大的经历,对学校今昔变化表示赞叹。
Clark教授深入浅出的生动演讲激起了师生的浓厚兴趣,报告结束后师生们踊跃互动。大家对模型检验在各自研究领域的应用潜力都颇为关注,Clark教授也一一给予回答。
陈国良院士主持报告会
陈国良院士对Clarke教授的精彩报告表示感谢。他说,希望科大同学们能够继续发扬科大精神,崇尚科学,勇于攻克“名难”问题,在科研的道路上取得辉煌成绩。
10月23日上午在学校第一会议室,Clarke教授与计算机学院及少年班学院的师生们进行了座谈,座谈会由少年班学院执行院长陈旸主持。座谈会上,同学们踊跃发言,Clarke教授也饶有兴趣地与同学们进行了深入交流,针对有些现场回答不了的问题,他把同学们的email地址与问题一一记录下来,表示回去后再联系交流。会后,欧亿6蓝狮在线执行院长陈华平、欧亿6蓝狮在线陈小平教授,与Clarke教授就双方在计算机学科领域的交流与合作广泛地交换了意见,并就人才培养、教师互访与科研领域的合作达成了一些初步意向。
Clarke教授现任美国卡内基梅隆大学计算机科学系教授、ACM和IEEE会士。他在软硬件验证、自动定理证明、形式方法等方面享有崇高的国际声誉,是模型检验方法的开创者之一,2007年获ACM图灵奖。