形式化方法教学在信息类学科教育中的重要性不言而喻。但是，此类课程对于多数学生而言，具有内容抽象、知识点繁杂、应用难度大、学习曲线陡等特点。这对从事形式化相关课程教学的教师提出了挑战。近来，有关我国的形式化方法教育现状调查结果指出，亟待加强专业教育中形式化方法的教学内容和改革。为此，chinasoft每年组织形式化方法教育论坛，旨在交流形式化方法相关课程的教学经验，探讨在计算机科学技术和软件工程等相关学科教学中加强形式化方法教育的途径，以促进形式化方法课程的教学发展。
01
论坛组织委员会
陈立前（国防科技大学）
谭添（南京大学）
02
论坛议程
03
论坛报告嘉宾简介
董威
报告题目：形式化方法教育中的工程思维能力培养
报告摘要：
形式化方法教育强调如何让学习者掌握基于数学和严格推理的方式保证软硬件系统的关键性质，但由于形式建模、形式验证等也是系统开发的有机组成，在当前系统规模越来越大、形式化方法理论依然有一定局限性的背景下，应该考虑将工程思维结合起来，让学生在未来实践中能够应对具有较大规模和复杂性的系统。该报告主要探讨在形式化方法相关课程教学过程中，如何更好将理论方法与工程思维能力有机结合，以培养学生能够在未来在工程实践中更有效地应用形式化方法。
报告人简介：
董威，国防科技大学计算机学院教授、博士生导师，中国计算机学会形式化方法专委会副主任、软件工程专委会执行委员，主要研究方向为高可信软件技术、智能化软件开发方法。入选教育部新世纪优秀人才支持计划，曾获中国计算机学会首届nasac青年软件创新奖、霍英东基金会高校青年教师奖等。多年来主讲研究生和本科的“形式化方法”、“软件工程”、“计算机辅助验证”、“软件工程方法与实践”等课程。先后主持国家和国防课题20余项，发表学术论文80余篇，出版国家级规划教材两部，相关成果应用于航空航天、装备控制、自主基础软件等关键领域。
黄文超
报告题目：《形式化方法导引》课程初探
报告摘要：
形式化方法以其严谨的数学基础，已成为保障网络系统、软件开发和芯片设计正确性与安全性的基石。与此同时，其他领域的技术也在快速发展，学生的兴趣更加多元化，这为形式化方法这门课程的教学带来了一定的挑战。再加上其较高的学习门槛，课程的顺利开展仍面临诸多考验。本报告将分享《形式化方法导引》课程在过去四年中的教学实践与探索，介绍如何通过优化课程设计，逐步激发学生对形式化方法的兴趣，力求在深度和易于理解之间找到平衡。同时，报告将总结课程中的经验与教训，并探讨未来进一步改进的方向，以应对教学中的各种挑战。
报告人简介：
黄文超，中国科学技术大学副教授，博士生导师。2006、2011年于中国科学技术大学计算机科学与技术系分别获得学士、博士学位。研究兴趣：形式化验证方法、网络安全、软件系统验证、芯片设计验证、区块链安全、android安全、移动计算等。在usenix security symposium、mobicom、ubicomp、infocom、tifs、jsac、tmc等多个国际知名会议和期刊上发表论文。开设本科生课程《形式化方法导引》和研究生课程《形式语言与计算复杂性》等。
汪宇霆
报告题目：形式化程序语义在程序设计教学中的应用
报告摘要：
程序设计是全国高校的必修基础课程，通常以c/c 等系统编程语言为载体，介绍结构化、面向对象、泛型编程等编程范式，以及训练学生设计编写中小型程序的能力。长期以来，程序设计课程中的重要基本概念（如指针、循环、递归等）通过非数学化的定义、以及典型示例程序来教授。由于这些定义和示例没有对基本概念进行精确描述，使得学生难以真正理解它们的原理、并在更广泛的编程实践中灵活运用。本报告介绍讲者将形式化程序语义融入程序设计教学的一些初步尝试。包括对基本概念进行更精确的数学化描述，设计对应教学示例，以求学生对它们有更直观和准确的理解。本报告还将介绍在概念精确性和易于理解方面所做出的一些取舍，学生对此的反馈，以及未来改进的方向。
报告人简介：
汪宇霆，上海交通大学john hopcroft计算机科学中心副教授，此前于美国耶鲁大学计算机系担任博士后研究员，博士毕业于美国明尼苏达大学双城分校计算机系。长期从事形式化方法方面研究，内容涵盖形式化验证和程序设计语言的理论基础（包括程序语义、逻辑框架等）以及它们在关键性系统软件（如编译器和操作系统）中的应用，代表性研究成果发表于形式化验证和程序设计语言的国际顶会（如popl、cav、oopsla等）。此外，还作为主要设计人员之一参与开发了基于高阶抽象语法的新型定理证明工具abella（http://abella-prover.org），其已被成功应用于程序设计语言学术界的多个研究项目。
苏亭
报告题目：软件分析与验证课程的教学探索
报告摘要：
软件分析与验证技术是从事软件工程和形式化领域学术研究的基础，也被业界广泛应用于构建软件开发环境和工具、解决相关实际问题。因此，如何让学生能够熟悉、掌握、运用、甚至改造相关软件（动态、静态）分析和验证技术是一项值得探索的教学工作。为此，我们近几年探索了一种包含理论介绍、课堂随测、动手实践、经典论文阅读为主要形式的教学方法，并结合我们研究小组的相关研究案例和工具进行加深理解。该课程也从面向研究生教学开始并逐步下沉至本科生的教学。这一报告将简要介绍我们在这一课程建设过程中的探索和初步经验。
报告人简介：
苏亭，华东师范大学软件工程学院教授，曾在新加坡南洋理工/瑞士苏黎世联邦理工担任博士后研究员。主要研究方向为软件工程、程序语言和软件安全，主要聚焦在复杂软件与系统（如工控软件、网络协议、编译器/程序分析器、移动应用软件等）的质量保障方面，其相关工作发表在pldi、oopsla、ccs、s&p、icse、fse等国内外重要会议和期刊上，部分技术成果被工业界测试工具集成并投入日常使用。曾获得ccf科技成果奖技术发明一等奖、ccf-蚂蚁科研基金“优秀应用项目”奖、四项ccf-a类国际会议的acm sigsoft杰出论文奖、google教授研究奖、世界前2% 科学家(2022-23)等。近几年在研究生和本科教学中探索软件分析与验证、软件工程理论与实践等课程的教学。
施晓牧
报告题目：定理证明公开课的收获：教学驱动交互式定理证明工具的发展
报告摘要：
今年开展了形式化方法公开课之定理证明，重点讲授了交互式定理证明工具coq的基础理论、工具使用以及在程序验证中的应用。本报告将从教学实践出发，回顾公开课的内容，展示通过和coq社区合作及开发教学工具以提升教学效果的成功案例，讨论在教学中工具理论与实践结合的重要性。同时探讨通过加强对coq背后理论的教学，特别是其基于的类型理论，帮助学生更深入理解coq工作机制，提升他们解决复杂问题和开发新证明技术的能力。通过加强对工具理论的理解，希望他们能够从工具应用者转变为理论贡献者和开发者，进而推动未来更先进的交互式定理证明器的研发。
报告人简介：
施晓牧，中国科学院软件研究所基础软件与系统重点实验室（计算机科学国家重点实验室）高级工程师。2014年获得法国格勒诺布尔大学计算机专业博士，曾在清华大学做博士后研究工作，2018-2022任深圳大学计算机与软件学院副研究员。长期从事基础软件形式验证研究，包括密码程序验证、硬件描述语言编译过程验证以及指令集模拟器的正确性验证等。相关研究成果发表在cav、ccs、ches等国际会议期刊上。负责中国科学院大学《形式化方法》课程中定理证明部分的教学工作。
印佳奇
报告题目：探索融入模型检测的软件工程数理逻辑教学体系
报告摘要：
高可信软件的验证正在成为当下可信软件安全领域的一个重要部分，传统的软件工程数学课程主要讲授数理逻辑，为加强软件理论和方法方向的教育以及培养本科生、研究生在软件理论基础和形式化方面的研究和应用的兴趣，课程教学设计引入模型检测示例辅助探索命题演算、谓词演算，以及程序语言的设计原理、程序分析和验证的基本概念和技术。这一报告将简要介绍引入模型检测的软件工程数理逻辑课程教学体系的设计，以及融入形式化方法的软件工程数学类基础课程开设的必要性。
报告人简介：
印佳奇，西北工业大学助理教授，中国形式化方法专委会执行委员。2022年获华东师范大学软件工程专业工学博士。研究兴趣：形式化方法、模型检测、程序统一理论、程序分析与验证、可信人工智能等。在fac、jsep、jcst、sqj、date、iceccs、tase等国际知名期刊和会议上发表多篇论文。开设本科生课程《程序设计基础》，和本硕共选课程《数理逻辑与程序设计原理》。
04
论坛组织委员会简介
论坛主席：陈立前
个人简介：
陈立前，国防科技大学计算机学院副教授。主要从事程序设计、形式化方法、软件工程相关教学科研工作。在acm/ieee transactions、popl、fse等期刊会议上发表论文多篇，获acm sigsoft杰出论文奖，出版教材译著4部。研究成果获省部级科技进步一等奖1项、二等奖1项。部分成果已在航天、国防等领域重大工程中应用。湖南省一流课程负责人，出版教材4部，获国防科技大学优秀教师奖，多次在全国性、省部级、校级教学比赛中获一等奖。
论坛主席：谭添
个人简介：
谭添，南京大学计算机学院助理教授，博士生导师。2017年博士毕业于澳大利亚新南威尔士大学，2017至2019年于丹麦奥胡斯大学从事博士后研究工作。研究方向为程序分析与程序设计语言。研究成果发表在toplas、pldi、oopsla、tosem、tse、fse、issta等相关领域的重要国际期刊与会议。程序分析框架“太阿”的作者。
