应2003网站太阳集团首页欢迎您的邀请，世界著名计算机科学家、计算机科学最高荣誉图灵奖获得者Edmund M. Clarke教授于10月21日上午莅临2003网站太阳集团首页欢迎您“信息技术与信息化”名家讲坛，为师生作了题为“形式化方法前沿问题”的精彩报告。
2003网站太阳集团首页欢迎您王捍贫教授首先向在座师生介绍了主讲人Clarke教授的研究领域和研究成果，并代表全院师生向Clarke教授的到来表示热烈的欢迎和衷心的感谢。Clarke教授现任美国卡内基梅隆大学计算机科学系教授、ACM和IEEE会士。他在软硬件验证、自动定理证明、形式方法等方面享有崇高的国际声誉，是模型检验方法的开创者之一，并于2007年获得计算机科学领域的最高荣誉ACM图灵奖。
形式化方法是基于数学和逻辑学的方法对计算机系统进行描述、扩展和认证的一种技术， Clarke教授的研究小组提出了一种“temporal logic model checking”的标准方法。在讲座中，Clarke教授介绍了形式化方法的一些旧研究，并讨论了这个领域的最新进展，介绍了bounded model checking 及其一些应用，以及如何安全应用numerical methods等。他对很多定义给出了数学描述，指出了efficient decision procedures的重要性，还介绍了当前为解决复杂问题对model checking进行扩展的趋势等。最后，Clarke教授表明该方法不仅限于理论上，在实际中也有很多应用。Clark教授深入浅出的报告将复杂的科学问题具体化、明晰化，激起了师生的浓厚兴趣，大家对模型检验在各自研究领域的应用潜力都颇为关注。
在提问交流环节，师生们踊跃提问，Clark教授也一一进行了回答。
报告结束后，仍有一些同学围绕着Clarke教授希望进行进一步的探讨，教授耐心回答并给同学们留下了联系方式，表示今后大家可进一步沟通联系。同学们用掌声对Clarke教授的精彩报告表示了感谢。
