北京大学信息学院2017年外教暑期课介绍和课程总结



2017年7月3日-14日,我院邀请了牛津大学的Anthony Lin副教授开设《逻辑与程序验证》课程。Anthony的主要研究方向为编程语言、形式验证等方面,这也与本次的课程内容有着较大的关联。来自我校各个院系的本科生以及留学生参与了这一课程,而Anthony则对于学生们的不同水平,用心的调整授课节奏,也经常与同学们交流课程中遇到的问题。

课程的内容先涉及简单的命题逻辑和谓词逻辑作为课程后半展开的基础;大多数同学对这一方面已有一定程度上的知识,因此课程进展很快;而在课程的后半段,内容涉及从约束求解的方法和应用到模型检查,对于同学们来说则是全新的内容;思维敏捷的同学们也提出了很多有价值的问题,在课堂上掀起了讨论的热潮。

Anthony作为课程的考核,交给同学们的是开放性的问题:自选题目,比较约束求解和传统方法之间的区别。同学们选择的问题都十分有趣而又不乏学术价值,在深入探究的过程中,不仅搞清了问题本身,也加深了对于约束求解方法的理解。

Anthony对于约束求解、程序验证方法的讲解,让同学们对于这一方面有了一定的认识,对于同学们在这一领域今后的科研、学习都有着不小的帮助。而同学们在课上的活跃也给Anthony留下了深刻印象,他也鼓励有兴趣的同学在这一领域做更加深入的研究。


图为Anthony(右一)和同学们的合照,因时间仓促未能全班一同合照,算是本次课程的一个小小遗憾吧。