教育论坛

形式化方法教育论坛

2022年11月27日 (13:30-17:00)



论坛简介

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

📢 【腾讯会议号】  173144092
📢 【直播链接】【点击观看视频直播】
📢 【B站直播】【点击观看B站直播】

论坛日程

时间 报告题目 嘉宾
13:30-14:00 理论与实践并重的程序分析教学 谭添
14:00-14:30 如何开展“轻型”的形式化方法教育 符鸿飞
14:30-15:00 课程和讲座之间:约束求解训练营回顾 蔡少伟
15:00-15:30 “形式化思维”从“大一入门课”抓起 胡振江
15:30-16:00 数理逻辑课程教学的一些尝试 陈翌佳
16:00-16:30 数理逻辑是计算机科学与系统的天然基础 - Formal Logic is the Calculus of Computer Science 刘志明
16:30-17:00 自由讨论

论坛嘉宾




1.论坛嘉宾:蔡少伟(中国科学院大学)

报告题目: 课程和讲座之间:约束求解训练营回顾

摘要: 学术讲座对于许多学生和科研人员都是重要的信息获取渠道。学术讲座的时间较短,比较适合方向内部交流或者概念性科普,但是不方便系统性地介绍一个研究方向。对此,集中一段时间学习的形式比如暑期班,短期培训班,也随之引起很多兴趣,特别是希望在某个新方向入门的老师学生或业界人员。我们尝试了一个更长周期的培训活动,以约束求解为主题,从理论,方法和应用进行系统讲解,该训练营共36课时,为期6周,每周一天周末,并且布置了相应的作业,配有助教。此次活动介于校内课程和短期培训之间,尝试以更长周期和作业等形式帮助学员更好地掌握课程知识。本报告将介绍本次约束求解训练营的组织工作,经验和教训,期待和大家一起讨论。

简介: 中科院软件所研究员,博导,中科院优秀导师,主要研究方向为约束求解、组合优化以及EDA(电子设计自动化)验证工具。提出了格局检测策略,有效解决局部搜索的循环现象,被广泛用于NP难组合优化问题。在命题逻辑可满足性问题(SAT)、可满足性模理论(SMT)问题、最大可满足性问题(MaxSAT)等国际比赛多次获得冠军,在国际EDA比赛获得亚军, 设计了搜索+推理的新型方法求解大规模组合优化问题,在多个著名NP难问题保持着前沿水平。在CAV,ICSE,AAAI,CP,SAT等会议以及AIJ, IEEE Trans. on Computers等期刊发表多篇论文,获得SAT‘2021最佳论文奖。他也致力于研究成果产业化,在EDA、软件验证、云计算、排班、智慧园区等领域展开了系列项目。




2.论坛嘉宾:陈翌佳(上海交通大学)

报告题目: 数理逻辑课程教学的一些尝试

摘要: 数理逻辑是计算机科学的源头之一,但主流的教学方式是将其作为离散数学的一部分。受课时的限制,很难让学生接触到数理逻辑中最深刻的一些内容。在过去几年里我们给上海交大致远学院单独讲授了这门课程,选择了面向数学系的教材。在这个报告中,我们会介绍选择这样教学内容的初衷,计算机专业学生接受的情况,以及一些对未来改进的思考。

简介: 上海交通大学计算机科学博士、德国弗莱堡大学数学博士。主要研究领域为逻辑、计算复杂性和算法图论,特别是参数复杂性和有限模型论。陈翌佳曾获微软青年教授奖,理论计算机国际会议ICALP’10及图论国际会议WG’17最佳论文奖,多次担任计算机科学中的逻辑研究旗舰国际会议LICS程序委员。陈翌佳讲授过的本科生课程包括《线性代数》《离散数学》《图论》《数理逻辑》《计算理论》《算法》《计算复杂性》。




3.论坛嘉宾:符鸿飞(上海交通大学)

报告题目: 如何开展“轻型”的形式化方法教育

摘要: 在近几年软硬件系统日益复杂的趋势下,形式化方法在保障系统正确性方面的重要性日趋凸显。然而,形式化方法其基于数理逻辑的特性导致在理解上对于不少学生过于晦涩,进而阻碍形式化方法教育的推广。在本报告中,讲者将主要以《模型检验》课程为例,讲解在教授该课程中如何“避重就轻”,在不引入过多逻辑负担的情况下,向学生传达模型检验中的主要概念、方法、以及部分学术前沿。此外,讲者也将分享如何通过在《离散数学》课程中插入少量可满足性求解算法(SAT)的内容以提升形式化方法在早阶段本科教育中的地位。

简介: 主攻形式验证的前沿理论,在概率系统模型检验、概率程序形式验证、循环不变式自动生成方面作出基础性理论贡献。先后在形式化方法以及程序语言理论国际著名学术会议及期刊POPL、PLDI、OOPSLA、CAV、ICALP、TOPLAS等发表二十余篇学术成果,涵盖可判定性、计算复杂性、验证算法以及相关数学理论等形式验证的各个基础理论层面。获2013年度信息物理系统形式验证国际学术会议HSCC最佳学生论文奖。概率程序形式验证方面的部分成果发表于由剑桥大学出版社出版的专著章节中。讲授课程包括《离散数学》、《程序分析与验证》、《程序语言理论》、《模型检验》等形式化方法相关课程。




4.论坛嘉宾:胡振江(北京大学)

报告题目: “形式化思维”从“大一入门课”抓起

摘要: “计算概论”是计算机专业大一学生的入门课。它不仅是讲授计算基础知识的引论课,更是培养学生形式化思维的一个重要环节。2019年,我和张伟老师在北大开设了基于函数式程序设计的“计算概论(实验班)”,旨在培养学生使用函数式思维进行程序设计和推理的基本能力,为学生将来从事算法设计、程序设计语言、软件验证等领域的研究建立比较好的理论基础。通过这门课,我们希望学生了解函数式程序设计语言的基本原理,熟练使用Haskell语言进行函数式程序设计,并熟练通过定理证明辅助器Agda对Haskell程序进行推理和变换。在这个报告中,我将和大家分享这门课的整体设计、讲授方法以及学生反馈。

简介: 胡振江,北京大学讲席教授、计算机学院院长。1996年在日本东京大学获得博士学位。曾担任东京大学信息理工学研究科教授和日本国立信息学研究所教授/系主任。长期从事程序设计语言和软件科学与工程的研究,曾获全日本最佳博士论文奖、日本软件科学会基础研究成就奖,被评为21世纪先驱科学家(日本科学技术振兴机构)、日本工程院院士、日本工学会会士、欧洲科学院院士、IEEE会士、ACM杰出科学家。




5.论坛嘉宾:刘志明(西北工业大学/西南大学)

报告题目: 数理逻辑是计算机科学与系统的天然基础 - Formal Logic is the Calculus of Computer Science

摘要: 根据个人回国几年讲授数理逻辑的一些经验和研究生招生与培养中的一些感受,讨论对数理逻辑和程序逻辑的基本概念和思想,揭示数理逻辑是计算机科学和系统的天然基础,建议数理逻辑基础应该在在本科低年级开设,而且由计算机科学专业的教授讲授,之后在程学设计与分析、数据结构预算法、数据库、软件设计与验证等课程中应该明确相应的逻辑和数学基础概念、思维和方法。实现这个愿望本身有多方面的困难和挑战,包括学管理方面和教学方面的相关领导和教师的认识统一、整体培养计划设计、各种课程授课教师的知识的基础性和系统性的要求等。愿以此讨论能够引起对计算机科学理论基础的教育和学习重视和兴趣。内容和观点一定有偏差和争议,供思考、讨论和批评。

简介: 刘志明教授长期从事软件理论和方法领域,尤其是形式化方法与模型驱动软件工程方法的研究。其主要成果包括基于模型/规约转化的容错程序设计与验证、概率时段演算(Probabilistic Duration Calculus)及可靠性规约和证明、和基于构件的形式化模型驱动软件工程方法rCOS。发表著作论文150余篇,发表在包括ACM Transactions on Programming Languages, Formal Aspects of Computing, Science of Computer Programming以及Theoretical Computer Science等在内的形式化方法领域主流期刊和会议上。其rCOS形式化方法曾获得第二届澳门特别行政区自然科学二等奖。




6.论坛嘉宾:谭添(南京大学)

报告题目: 理论与实践并重的程序分析教学

摘要: 程序分析是一门实践性很强的技术,但其理论到实践的跨度较大,是阻碍学生真正系统性掌握该技术的主要难点。李樾老师和我在南京大学开设《软件分析》课程,目标是讲授程序分析理论知识的同时,也培养学生将理论知识运用到实践场景的能力。为此,我们基于自研Java程序分析平台“太阿”,设计了一系列涵盖多种分析技术且相互关联的实验作业,帮助学生在实践中加深理解对课程中重要且实用的理论知识。在这个报告中,我将和大家分享我们如何设计实验作业并通过实验帮助学生巩固理论知识并提高实践能力。

简介: 谭添,南京大学计算机科学与技术系副研究员。2017年于新南威尔士大学获博士学位,2017至2019年于奥胡斯大学从事博士后研究工作。主要研究方向为程序分析与程序设计语言。研究成果发表在TOPLAS、PLDI、OOPSLA、ECOOP、TOSEM、FSE等相关领域的国际著名期刊与会议。讲授课程包括《软件分析》、《编译原理》。



论坛主席





1.论坛主席:贺飞(清华大学)

简介: 清华大学长聘副教授,博士生导师。主要从事程序验证、模型检验和自动推理的研究。开发了模型检验和软件验证工具,并应用于国家重大安全领域。在包括POPL, CAV, PLDI, OOPSLA, PPoPP, ICSE, ESEC/FSE, ASE等在内的国际重要会议和期刊上发表论文70余篇。现任《Theory of Computing Systems》编委,《Frontiers of Computer Science》青年副主编,曾/现任ICSE, ESEC/FSE, CONCUR, FMCAD, SAT, ATVA, APLAS, ICECCS, SETTA等国际学术会议程序委员会委员。系CCF形式化专委会常务委员,曾获2008年度CCF优秀博士学位论文提名奖、ASE 2018 Distinguished Paper、PPoPP 2022 Best Paper奖等。






2.论坛主席:熊英飞(北京大学)

简介: 熊英飞于2009年从日本东京大学获得博士学位,2009-2011年在加拿大滑铁卢大学工作,2012年加入北京大学,现任新体制长聘副教授。熊英飞的研究兴趣是程序设计语言和软件工程,特别是程序合成、修复和分析。他提出了理论和方法降低程序编写和缺陷修复的代价。比如,基于差别的双向变换框架是最广泛使用的双向变换框架之一,概率和逻辑结合的程序合成框架玲珑框架将程序修复的正确率从此前不到40%提升到80%以上。他的工作也被工业界采用,比如新一代Linux内核配置项目、燕云DaaS系统、华为公司等。他获得CCF-IEEE CS青年科学家奖、MODELS十年最有影响力论文奖,5次获得ACM SIGSOFT/IEEE TCSE杰出论文奖。他是SATE18的程序委员会联合主席,也在ICSE、FSE、ASE、ISSTA等会议担任PC。