4月15日，应中科大—耶鲁高可信软件联合研究中心邀请，德国慕尼黑理工大学的Christian Urban博士来我院进行访问，并作题为 “Verifying A Regular Expression Matcher and Formal Language Theory”的学术报告。计算机学院冯新宇教授主持报告会，计算机学院部分师生参加了报告会。
Christian Urban博士2000年毕业于英国剑桥大学并获博士学位，随后在剑桥大学、普林斯顿大学和慕尼黑理工大学等多所国际著名院校和研究机构从事程序语言理论、定理证明器以及编译器相关的研究工作。Christian Urban博士是著名定理证明器Isabelle的核心开发者之一，近年来主要关注自动定理证明、程序语言等理论领域，已在国际顶级学术会议和期刊上发表多篇论文。
Christian Urban博士为师生们介绍了机器可检查的证明在计算机理论研究和程序验证中的重要性，讲解了Isabelle中相关算法的实现，以及如何使用逻辑语言来形式化地严格证明算法的正确性。Christian Urban博士还重点介绍了与国内高校合作所取得的最新成果——如何应用Isabelle来证明自动机理论领域中的Myhill-Nerode 定理。这一成果将在知名国际会议Interactive Theorem Proving 2011上发表。
4月25日，Christian Urban博士还访问了中科大—耶鲁高可信软件联合研究中心的苏州实验室，与师生们进行了更深入的交流。他分析了Isabelle与其它定理证明器的不同之处，并热情回答了同学们的提问。他还兴致勃勃地向师生们展示了Isabelle工具的使用和特点。最后，Christian Urban博士还表示了未来进行深入合作的意向。
Christian Urban博士与师生们座谈 
Christian Urban博士正在展示Isabelle定理证明器的使用
