形式化方法教育论坛

FMAC

教育是形式化方法持续发展的重要支撑。然而，形式化方法学习曲线长，高强度运用有着较高的门槛，严重制约了形式化方法在软件和系统开发与演化中的广泛应用。近来，有关我国的形式化方法教育现状调查结果指出，亟待加强专业教育中形式化方法的教学内容和改革。为此，FMAC 2020会议组织了本次形式化方法教育论坛，旨在交流形式化方法及相关课程教学方面的经验，探讨在计算机科学技术和软件工程等相关学科教学改革中加强形式化方法教育的途径。

论坛组织委员会（主持人）：

王 戟（国防科技大学）

孙 猛（北京大学）

日程安排：

时 间：2020年11月20日（星期五）14:00-17:30

地 点：重庆富力假日酒店 会议室3

论坛议程：

报告及嘉宾简介：

1. 裘宗燕：有关形式化方法教育的一些思考

摘要：我们都感觉形式化方法在普遍性的计算机教育中没有得到应有的重视，这个情况应该如何看待、如何理解？实际上，这个问题牵涉到形式化方法本身在计算机科学技术中的地位和潜在作用，以及它在计算机专业学生成长中的意义和价值。本报告将对这些方面的问题和情况做一些梳理和分析，并就相应的可能措施和前景提出一些看法。

简介：裘宗燕，北京大学数学学院教授（退休），CCF杰出会员。关注的主要领域为软件理论、形式化方法、程序语言及其理论基础等。

2.  傅育熙：理论与形式化方法的课程建设与教材建设

简介：傅育熙，1992年获英国曼彻斯特大学计算机博士学位，1994年起在上海交通大学计算机系任职，现为上海交通大学特聘教授。研究领域为理论计算机科学，研究内容涉及程序理论、并发理论、等价性验证、可达性理论、交互理论。是国家杰出青年基金获得者、上海市优秀学科带头人。2000-2009年任上海交通大学计算机系主任，2001-2013年任上海交通大学软件学院院长。学术兼职有：上海高校软件理论研究中心主任、国务院学位委员会第六届学科评议组成员（2010-2014）、上海市计算机学会理事长（2015-2018）、教育部计算机类专业教学指导委员会副主任（2013-2017，2018-2022）。是Mathematical Structures in Computer Science的编委。

3.  李希萌：研究生课程《形式化验证》教学探索

摘要：形式化验证课程是形式化方法方向的先导性课程，在该方向的研究生培养体系中占有重要地位。从研究生教学特点和形式化验证课程的自身特点出发，探讨在研究生课程中开展形式化验证的教学方法。结合多年来研究生课堂教学实践，从课程定位、教学内容设置、教学形式和考核方式等方面，对研究生形式化验证课程教学做了初步探索，给出了相关经验总结。

简介：李希萌，首都师范大学讲师，硕士生导师。在丹麦技术大学取得博士学位，并曾在欧盟项目SESAMO、德国项目CRISP下参与形式化方法、信息流安全验证方面研究。现主要研究方向为区块链程序、架构的形式化验证，在该方向获批国自然青年项目一项，北京市教委项目一项，在ESORICS、ICFEM、APLAS等CCF会议和LMCS、COLA等SCI期刊发表论文十余篇。

4.  卜磊：曲高而和不寡的形式语言与自动机

摘要：形式语言与自动机一课是计算机理论方向的重要基础课程，也是长期被计算机方向学生视为“艰深难懂”的硬核课程。 南大计算机系同样对此课程给予了高度重视，在15年将此课程列为了计算机科学方向核心课程之一。相关教学团队也展开了积极的教学改革与尝试。从15年的仅有9个学生到今年的100多人选课，学生们不再看到课程名就避而远之，而是口耳相传，越来越多学生在“应用”浪潮下主动来探索基础原理，取得了可喜的效果。本次报告我们将介绍教学团队近年来在相关课程上所作的教改尝试以及得失，并请各位专家、老师批评指正。

简介：卜磊，南京大学计算机科学与技术系教授，博士生导师。长期从事计算机理论基础和程序设计课程教学，获评南京大学创新育人奖、南京大学本科生实践教学优秀指导教师、计算机系毕业生“我心目中的好课程"等；研究工作主要围绕大规模复杂软件的可信保障，在实时混成系统形式验证方面取得系列创新性结果，发表在《中国科学》、IEEE TC、IEEE TCAD、ACM TCPS、RTSS等，自研工具已在列控、航天、物联网等领域得到应用验证，被写入国际权威教科书，获NASAC青年软件创新奖等。

5.  邓玉欣：形式逻辑教学体会

摘要：形式逻辑是形式化方法教学的重要主题之一。在过去几年中，本人利用定理证明器Coq作为实验工具来讲授命题逻辑、谓词逻辑、归纳思维、形式化证明、以及函数语言程序设计基础等内容。在此次报告中，将与大家交流这方面的教学体会。

简介：邓玉欣，华东师范大学软件工程学院教授，博士生导师，副院长。分别于1999年和2002年获上海交通大学学士和硕士学位，2005年获法国巴黎国立高等矿业学院博士学位，之后在澳大利亚新南威尔士大学从事博士后研究。2006年至2015年任上海交通大学计算机系副教授。2011年在美国卡内基梅隆大学计算机系访问。自2012年至2014年在联合国教科文组织教育部门任借调专家。2015年至今在华东师范大学任教。

主要研究领域包括概论计算模型、量子计算模型、程序语言理论。代表性工作包括一个被国外学者写进并发理论教科书的Deng Lemma和关于概率并发理论的一部英文专著。在国际学术刊物和会议发表论文70多篇，是TASE 2016，FMAC 2017程序委员会共同主席，担任ICALP 2013，ICALP 2016，ICALP 2018，CAV 2021等会议的程序委员会委员，目前是上海市计算机学会理论计算机科学专委会主任，中国计算机学会高级会员。

6. 张文辉：形式化方法课程教学与思考

摘要：报告内容主要介绍中国科学院大学研究生形式化方法课程的基本情况、课程内容，以及课程内容的变化和学生反馈与教学思考等，对课程内容和教学进行交流讨论。

简介：张文辉，中科院软件所计算机科学国家重点实验室研究员、中国科学院大学岗位教授。主要研究兴趣包括形式模型、数理逻辑与程序逻辑、程序性质的推理与模型检测、计算机软件正确性的理论与方法，具体工作包括基于限界正确性检查和不动点算法的检查离散迁移系统CTL性质的模型检测工具VERDS的相关理论研究与算法实现。

7.  宋富：编译原理教学经历分享

摘要：上海科技大学是2013年成立的小规模学校，计算机课程体系尚在完善过程中，因此，形式化验证相关的数理逻辑、形式语言与自动机等课程都没有开设。本次报告将分享本人在编译原理教学经历，包括如何提高学生的编译原理基础理论知识和实践动手能力，以及如何开拓学生在形式化验证相关方面的知识面。

简介：宋富，上海科技大学信息学院助理教授，上海科技大学系统与安全中心主任，研究领域包括模型检查、系统自动分析与验证及在系统安全方面的应用，近4年承担编译原理和计算理论的教学。