4月25 日,应我院中科大-耶鲁高可信软件联合研究中心邀请,德国慕尼黑理工大学的Christian Urban博士来中科大苏州研究院访问。
Christian Urban博士于2000年在英国剑桥大学获博士学位,随后在剑桥大学、普林斯顿大学和慕尼黑理工大学从事定理证明相关的研究工作。他是著名定理证明器Isabelle的核心开发者之一,近年来主要关注自动定理证明、程序语言等理论领域。
Christian Urban博士向研究中心师生做了关于Isabelle的精彩介绍。在讨论会上,他剖析了Isabelle的各个方面,并分析了Isabelle与其它定理证明器的不同之处,热情地回答了学生们提的诸多问题。同时,他还兴致勃勃地向师生们展示了Isabelle工具的使用和特点。通过一下午的交流,Christian Urban博士和实验中心的老师学生还对各自的研究方向进行了深入的探讨,并达成了长期合作交流的共识。
Christian Urban博士与研究中心邵中教授(耶鲁大学)在讨论未来的合作计划
Christian Urban博士正在展示Isabelle定理证明器的使用
Christian Urban博士与研究中心学生座谈