应北京大学信息科学技术学院的邀请，世界著名计算机科学家、计算机科学最高荣誉图灵奖获得者Edmund M. Clarke教授于10月21日上午莅临北京大学“信息技术与信息化”名家讲坛，为师生作了题为“形式化方法前沿问题”的精彩报告。
北京大学信息科学技术学院王捍贫教授首先向在座师生介绍了主讲人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教授的精彩报告表示了感谢。
