形式化方法教育论坛
|
|
|
| 扫码加入腾讯会议 | 扫码观看论坛视频直播 | 扫码进入B站视频直播 |
形式化方法教学在信息类学科教育中的重要性不言而喻。但是，此类课程对于多数学生而言，具有内容抽象、应用难度较大、知识点繁杂等特点。这对从事形式化相关课程教学的教师的提出了挑战。为此，ChinaSoft 2021会议组织了本次形式化方法教育论坛，其目的于交流形式化方法的课程教学经验，探讨信息类相关学科中形式化方法教育的途径，以期促进形式化方法课程的教学。
论坛组织委员会：
邓玉欣（华东师范大学）
刘万伟（国防科技大学）
日程安排：
时间：2021年12月25日（星期六），14:00~18:00
论坛议程：
论坛报告嘉宾简介：
1. 报告人：刘志明
摘要： 根据个人的一些经验和观察，浅谈自己对形式化方法教育的内容、形式和效果方面的问题。这些问题能不能反应最近几年形式化方法教育的情况，但是可能对现在形式化方法以及整个计算机科学和软件工程学科的研究和教学现状有一定的影响。一些观点一定有偏差和异议，仅供思考、讨论和批评。
简介： 刘志明，西北工业大学教授、博士生导师、智能嵌入式系统研究中心（CiES）主任，兼任西南大学讲席教授和软件研究与创新中心（RISE）主任。1988年在中科院软件所获得硕士学位，1991年从英国华威（Warwick）大学获计算机科学博士学位。 主要研究方向为软件基础理论、可信软件方法、基于人机融合系统的计算与人工智能的综合理论以及软件架构。主要代表性学术成果有基于模型转换的容错和实时程序设计方法；用于系统可靠性分析的概率时段演算；rCOS形式化模型驱动软件开发方法；人机物融合系统软件体系架构建模理论与方法。
2. 报告人：赵建华
摘要： 在算法、数据结构、编程等的课程教学中，教师仍然会讲解为什么某个算法、数据结构、程序可以完成预定的功能。这些论述过程实际上是一种非形式化的证明过程。这个过程实际上是证明的主干部分，按照形式化的要求将其中步骤补足之后，就可以得到形式化的证明。但是，在不同的教材中会以不同的风格进行论证，有时同一本教材也会有不同的论证风格。本次报告我将讨论按照统一风格来进行算法、数据结构、程序论证的可行性。同时，也讨论了课堂讲授时需要适当控制证明的形式化程度，以免形式化论证过程中的细节掩盖了讲课的主线。
简介： 1999年3月毕业于南京大学计算机科学与技术系，同年5月获得博士学位。现为南京大学计算机科学与技术系教授。主要研究方向为形式化方法与软件工程。1998年到联合国大学国际软件技术研究所（澳门）学习研究，主要方向为形式化方法。主持或作为骨干成员参与了包括973项目，863项目，国家自然科学基金项目在内的多项科研项目。两次获得教育部科技进步二等奖2005 年入选教育部新世纪人才培养计划、江苏省青蓝工程学术骨干培养计划.在国际国内学术会议和学术期刊发表科研论文30余篇。
3. 报告人：张立军
摘要： 讨论模型检验教学经验，如何调动学生的积极性，使学生在适当的时候思考和讨论。特别是怎么从沉默的学生群体那里获得有价值的反馈。这更具备挑战性，因为他们在大多数情况下都犹豫不决，但是他们的反馈更有价值。讨论如何通过英文课件、教科书及练习，培养学生能够基本英文阅读、理解能力。讨论理论、工具、案例等在教学中的如何应用。
简介： 张立军博士，中科院软件所研究员，中国科学院大学特聘教授。2008年德国萨尔大学博士毕业。任形式化方法欧洲顶级国际会议LICS执行委员会委员，CONCUR、TACAS等主席，人工智能会议AAAI等的程序委 员会委员。 在形式化方法、程序语言/软件工程、人工智能 等领域权威学术会议与期刊上发表论文80余篇， 带领团队开发多个验证工具。
4. 报告人：赵永望
摘要： 在本科生、研究生课程以及面向工业界的培训课程中推广形式化方法教育，是国内形式化方法普及的重要途径之一。本报告主要从本科生、研究生、工业培训等方面，介绍讲者在形式化方法教育方面的一些实践与想法，包括讲者在《离散数学》《形式语言与自动机》等本科生课程中融入形式化方法及教育工具，在讲者课题组的研究生中组织实施形式化方法工程项目，在面向工业界进行形式化方法培训，以及面向教育的形式化方法与工具的国内外现状。最后，讨论形式化方法教育的一些想法。
简介： 赵永望，浙江大学 教授/博士生导师，移动终端安全浙江省工程实验室主任，工信部重大专项首席科学家，中国计算机学会(CCF)杰出会员。担任ARINC653国际操作系统标准委员会委员、CCF系统软件专委会和形式化方法专委会委员、国际标准化组织 ISO/IEC JTC1 SOA研究组组长等。主要研究方向包括形式逻辑与验证、操作系统安全、编程语言原理等。主持和参与国家自然基金重点项目、工信部重大专项、载人航天工程重点项目等二十余项，2011和2017年分别获得中国电子学会和山东省科技进步一等奖。
5. 报告人：熊英飞
摘要： 传统理论类课程存在的弊端是很多时候同学并没有理解形式系统工作的基本原理和方法，而是在证明的时候通过直觉写下类似“显然可得”的一些步骤，这样的证明通常也会被认为是正确的。过去的教学实践表明，常常有同学已经读到研究生仍然不能搞清楚一些基础数学符号的含义或者证明理论中的基本概念。
北京大学从2020年开始增设了一门软件理论方面的基础课程，试图通过一门课概览软件理论的内容（数理逻辑、形式语义、类型系统等），然后后续其他课程再深入学习。借这个机会，胡振江、熊英飞等教师尝试了引入美国宾夕法尼亚大学Benjamin Pierce等人牵头撰写的《Software Foundations》一书作为教材。该教材的主要特点是书中的定理和证明全部用Coq编写，同学们做习题的时候如果步骤不能完全正确就不能通过编译，确保同学们正确理解不能含糊通过。
本次报告分享该课程过去一年实践中的一些经验教训，也有一些开放问题和各位专家讨论。
简介： 熊英飞于2009年从日本东京大学获得博士学位，2009-2011年在加拿大滑铁卢大学工作，2012年加入北京大学，现任新体制长聘副教授。熊英飞的研究兴趣是程序设计语言和软件工程，特别是程序分析、综合和修复。他提出了理论和方法降低程序编写和缺陷修复的代价。比如，结合概率和逻辑的程序合成框架玲珑框架大幅提升了错误修复的正确率，基于差别的双向变换框架是最广泛使用的双向变换框架之一。他的工作也被工业界采用，比如新一代Linux内核配置项目、燕云DaaS系统、华为公司等。他是SATE18的程序委员会联合主席，也在ICSE、FSE、ASE、ISSTA等会议担任PC。
6. 报告人：贺飞
摘要： 软件学科的传统教学体系中存在基础课程与应用课程衔接不够紧密的问题。一方面，同学们学完数理逻辑等基础课程后不知其具体用途；另一方面，同学们学了很多编程语言，却不知道这些程序语言背后的原理是什么。本课程于2017年筹备，2019年面向清华大学软件工程专业大三年级学生正式授课。主要设计了三部分教学内容，即形式逻辑、判定过程和程序验证。通过这些内容的讲解，希望帮助同学们建立起程序语言和形式逻辑之间的联系，加深对程序的深层次理解，进而具备编写更有效、更安全、更可靠软件代码的能力。本报告将分享该课程在教学、实验等过程中的一些经验和教训，也有一些开放问题和各位专家讨论。
简介： 贺飞，清华大学长聘副教授，博士生导师，CCF形式化专委会常务委员。主要研究程序验证理论、方法、工具及应用。开发了模型检验和软件验证工具，并应用于航空、航天、高铁等国家重大安全领域。任《Theory of Computing Systems》编委，ICSE, ESEC/FSE, CONCUR, FMCAD, SAT, ICECCS, SETTA等国际学术会议程序委员会委员。
7. 报告人：曹钦翔
摘要： 在过去几年中，本人利用定理证明器Coq作为教学、实验工具来讲授形式语义理论，以及离散数学课程中的一些关于公理集合论的内容。在此次报告中，本人将与大家交流这些教学探索中的体会。
简介： 曹钦翔，本科毕业于北京大学，博士毕业于美国普林斯顿大学，2018年回国任教，现为上海交通大学约翰霍普克洛夫特计算机科学中心副教授、博导，2019年入选上海市浦江人才计划。曹钦翔长期从事基于交互式定理证明的程序验证工具开发，并研究有关程序逻辑特别是分离逻辑的理论问题。曹钦翔是Verified Software Toolchain（VST）工具的主要开发者之一，该工具首次实现了从业务逻辑，到源代码开发，再到编译的全链条正确性验证。
论坛组织委员会简介：
1. 论坛主席：邓玉欣
简介： 邓玉欣，华东师范大学教授，软件工程学院副院长，上海市计算机学会理论专委会主任。主要研究方向包括并发计算模型和程序理论，代表性工作包括一个已经被国外学者写进教科书的“邓引理”(Deng Lemma)和关于概率并发理论的一部英文专著。发表学术论文75篇，多篇出现在国际权威期刊和会议如Information and Computation、Theoretical Computer Science、ICALP、LICS、POPL等。曾为CONCUR 2018作特邀报告。
2. 论坛主席：刘万伟
简介： 刘万伟，国防科技大学教授，CCF 高级会员。主要研究领域为形式化方法、自动机理论、AI算法形式验证等。研究成果发表在TSE、ASE、ICSE、IJCAI等国际期刊/会议上。在TACAS工具验证比赛中多次获得冠军。长期从事形式化方法基础理论的教学，为本科生、研究生讲授《抽象代数》、《数理逻辑》、《计算理论》、《计算机逻辑学》等课程。