2009年10月16日上午10点，应软件工程技术研究开发中心的邀请，图灵奖获得者美国卡内基梅隆大学Edmund M. Clarke教授做客软件所并做了一场题为“Model Checking: My 28-year Quest to Overcome the State Explosion Problem”的学术报告。冯玉琳研究员主持报告会。
　　Clarke教授的报告从Intel芯片的实际需求出发，引出model checking的问题和工作原理，重点解释了处理状态爆炸问题的主要技术。他的演讲图文并茂，生动的表达了他将状态进行合并，然后映射到一个更小的状态集合的思路，他还分析了这种解决方法的优点与缺点，对于该方法的缺点，比如会产生转换错误的问题，他又继续提出了自己的解决方法。演讲的最后他对未来进行展望，提出一些model checking未来的研究方向。
　　他的演讲叙述清晰，加上文字、图片和动画的辅助，让在座的听众都能够很好的理解，并从中感受到他27年来对该领域所付出的努力。
　　Clarke教授1967年Edmund M. Clarke在弗吉尼亚大学获得数学的学士学位，1968年在杜克大学获得数学硕士学位，1976年在康奈尔大学获得计算机博士学位。然后，Clarke 在杜克大学任教两年，1978年加入了哈佛大学并担任助理教授。1982年，Clarke加入了卡内基梅隆大学计算机系，并在1989年被评为全职终身教授。
　　Clarke教授曾任Formal Methods in Systems Design杂志主编。曾任荣获2004年IEEE Harry M. Goode纪念奖。ACM和IEEE计算机学会会士，2005年当选美国工程院院士。并于2007年获得图灵奖。