CCF软件大会2026|形式化方法教育论坛

一、论坛背景

形式化方法教育论坛是专注于形式化方法教学改革的核心特色论坛，本次论坛汇聚国内多所高校的教育工作者，围绕形式化方法课程的抽象内容难点、工程思维融合、数理逻辑教学体系重构等核心议题，通过主题报告和经验分享等形式，交流课程设计、工具开发、人才培养的一线实践成果。该论坛的重要性在于直面当前信息类学科中形式化方法学习曲线陡、学生应用能力薄弱的普遍痛点，精准对接关键软件领域对高可信技术人才的迫切需求，促进国内同行对形式化方法系统化教学的深入交流。其长远意义在于持续推动国内计算机、软件工程学科完善形式化方法教育体系，打通理论教学与产业落地的壁垒，培养更多兼具严谨数学推理能力与工程实践能力的核心人才，助力软件产业高质量发展。

二、论坛组织委员会

• 邓玉欣（上海财经大学）
• 李晓红（天津大学）
• 曹钦翔（上海交通大学）

三、论坛安排

日程安排：

时间：2026年11月6日，09:00-12:00

地点：天津市社会山国际会议中心酒店，二层6号会议室

论坛议程：

四、论坛报告嘉宾简介

1. 报告人：蒋炎岩（南京大学）

题目：教学生如何“说话”的探讨

摘要：《离散数学》课程承担着计算机专业学生理论基础启蒙的重要任务。然而，经典教学体系往往将逻辑、集合、代数结构、图论等多个主题并置呈现，知识点彼此跨度较大，既给教师组织教学带来困难，也容易使学生陷入“会做题，却不知道为什么学”的困境。本报告探讨一种以形式化方法为主线的教学路线，通过引入形式化语言、形式化推理以及适当的工具支持，帮助学生逐步建立计算机科学中“精确地说话、精确地思考”的基本能力，为后续程序设计、算法、系统与软件工程等课程打下基础。

简介：蒋炎岩，南京大学副教授，研究方向为系统软件和软件自动化。蒋炎岩曾多次获得操作系统/软件工程领域 CCF-A 类会议论文奖，作为程序委员会主席主持了 ChinaSys'25 研讨会，并担任了多个操作系统/软件工程领域顶级会议的程序委员会委员。蒋炎岩执教了广受欢迎的《操作系统》课程，曾获 “南京大学我最喜爱的老师” 荣誉，至今互联网课程视频播放量已超过500万次。

2. 报告人：刘万伟（国防科技大学）

题目：论 AI 时代形式化方法课程教学的挑战与机遇

摘要：形式化方法课程具有理论抽象、逻辑严密、实践性强的特点。随着人工智能尤其是大模型技术快速普及，计算机类课程的教学范式、学生学习方式与行业人才需求发生深刻变革，传统形式化方法教学模式的局限性日益凸显。本报告从 AI 时代形式化方法方向的特点出发，分析大语言模型对于形式化方法课程的学习以及科学研究的影响，讨论 AI 时代对教师在本科生教学、研究生科研指导带来的挑战及应对建议。

简介：刘万伟，国防科技大学计算机学院教授、博士生导师，主要研究方向为形式化方法、高可信软件、智能软件可靠性。近年相关研究成果发表在 TOSEM、TSE、TPAMI、TKDE、JSCP、NN、Sci-China、JCST、IPL 等国际/国内期刊以及 ICSE、CAV、ASE、ISSTA、NeurIPS、IJCAI、TACAS、ACM MM、ICME、ATVA 等国际会议上。长期躬耕教学一线，为本科生、研究生讲授计算机程序设计、计算理论、抽象代数、数理逻辑等课程； 著有《高级范畴论》等三部教材， 并译著一部教材。

3. 报告人：李建文（华东师范大学）

题目：AI时代模型检查课程的教学探索

摘要：大模型技术的飞速发展使得学生现在不管是学习、做作业还是写代码都高度依赖AI工具来完成。这样造成的直接后果就是，学生上课不用再听讲、作业不用再自己做、代码也不用再自己写：他们唯一要做的就是对着prompt敲几行指令。这就对我们教师的授课带来了巨大的困难和挑战。在本报告中汇报人将介绍自身所教授课程的经历和一些思考，希望能和广大同行共同探讨如何在大模型时代上好大学的课堂教学。

简介：李建文，华东师范大学软件工程学院教授，博导。主持国家自然科学基金面上、青年项目、参与重点项目。研究方向主要为形式化自动验证技术，可用于保障计算机软硬件系统的正确性和安全性，重点应用场景包括芯片、航天、轨道交通等安全攸关领域。

4. 报告人：王迪（北京大学）

题目：大模型时代的编程语言理论教学

摘要：大模型的快速发展对编程语言理论相关课程（如编译原理、类型系统、语言设计等）的教学带来了多方面的冲击。一方面，大模型的编程能力使得传统的课程项目设计带来了挑战，在大模型可以轻松完成既有的编程任务的背景下，我们需要迅速地调整课程的教学目标、重塑课程项目设计。另一方面，大模型在编程能力上的演进也使得编程语言本身受到挑战：编程语言的选择是否还重要？我们是否还需要改进已有的编程语言，或者发明新型的编程语言？如果需要，大模型时代，编程语言的重心应当如何改变？在报告中，我希望把编程语言重新定位为人-大模型-机器的三方契约，从三方协同的角度探讨编程语言的发展，并以此为基础讨论教学方式的改变。

简介：王迪，北京大学计算机学院助理教授。他于2022年在美国卡内基梅隆大学获得博士学位，于2017年在北京大学获得学士学位。他的研究兴趣包括形式化验证、程序分析、类型系统以及概率编程，目前的研究项目涉及资源安全的系统编程、可编程贝叶斯推断、量化程序分析以及面向证明的编程语言。他获得了国家优秀青年科学基金项目（海外）资助，多项研究成果发表于编程语言领域的顶级会议POPL、PLDI、OOPSLA、ICFP等。他是中国计算机学会形式化方法专委会执行委员。

5. 报告人：林云（上海交通大学）

题目：从“代码编写”到“需求编译”：AI智能体驱动下的软件工程教学演进与前沿探索

摘要：在生成式AI以前所未有的速度重塑代码生成的今天，传统软件工程正面临从“代码编写”向“需求定义”与“质量约束”转移的范式迁移。本次报告将结合教学实践与科研探索，分享这一演进过程中的一线经验。首先，报告将回顾2025年秋季在上海交大IEEE试点班的教学改革，探讨如何通过引入测试驱动开发（TDD）和面向智能体的领域特定语言（DSL）建模，引导学生从代码工人转型为智能体架构师，指挥多智能体复现12306等复杂核心业务，实现软件工程概念与底层编码的彻底解耦。其次，针对大模型在处理复杂多模态需求文档时易产生的幻觉与遗漏痛点，报告将介绍旨在突破“复杂性高墙”的ARC（Agentic Requirement Compilation）需求编译框架。该框架模拟经典V模型构建双向测试驱动引擎，实现自顶向下的可测试架构构建与自底向上的约束代码生成，通过轻量级图结构DSL与全链路追溯机制，将包含50-200个场景的需求文档编译为可运行的Web系统，并在GUI测试通过率上较主流基线平均提升50.6%。最后，报告将剖析当前AI编程的“马太效应”与调试测试痛点，并展望形式化方法和大模型在课堂和工业界落地实践。

简介：林云，上海交通大学计算机科学与技术系副教授，系副主任，博士生导师，原新加坡国立大学助理教授（研究岗），入选国家海外高层次青年人才计划、华为x-explore人才计划。研究方向包括自动编程、可解释AI、网络反诈等，获ICSE2018杰出论文奖，及多次中国软件大会原型研究奖。ICSE、FSE、USENIX Security等重要国际会议的程序委员会委员。主持国家自然科学基金委海外优青项目及面上项目和多项校企合作。自动编程技术落地于豆包代码模型以及Trae IDE，GUI测试相关研究入选信通院优秀案例等。

6. 报告人：陆旭（西安电子科技大学）

题目：从拔尖到普适：基于《计算复杂性理论》的形式化思维教学实践

摘要：形式化方法教育不仅需要帮助学生掌握数学基础和严格推理方法，也需要培养学生将形式化思想应用于计算机科学问题分析和解决的能力。本科理论课程是开展形式化思维培养的重要载体，但对于计算机专业学生而言，如何将抽象的形式化概念、数学推理与具体问题建立联系，是课程教学中的一个重要问题。该报告结合西安电子科技大学《计算复杂性理论》课程的教学实践，介绍从拔尖班到普通班开展教学过程中对形式化思维培养的一些探索，重点讨论如何通过计算模型、问题规约、复杂性分析和严格证明等教学内容，将形式化建模与逻辑推理融入本科理论课程，并探讨面向不同学生群体开展形式化教育的教学方法与实践。

简介：陆旭，西安电子科技大学副教授、博士生导师，主要研究方向为形式化方法、程序验证、模型检测、智能决策与智能软件构造。主持国家自然科学基金面上、青年、博士后科学基金等项目，作为核心成员参与国家自然科学基金重大、重点项目等科研任务。近年来发表学术论文多篇，相关成果发表于TKDE、TPDS、TITS、ASE、AAAI等顶级期刊和会议。近年来承担本科生《计算复杂性理论》课程教学，先后面向计算机科学与技术专业拔尖班和普通班开展教学实践。

7. 报告人：白光冬（香港城市大学）

题目：神经网络鲁棒性验证

摘要：随着深度神经网络模型在自动驾驶等重要及安全关键领域中的应用，模型在面对复杂环境、恶意扰动和未知输入时能否保持稳定、可靠的性能，已成为可信人工智能发展所面临的重要挑战。如何理解和验证模型的鲁棒性，是形式化方法在人工智能安全研究的重要课题。本报告将介绍我们在模型鲁棒性验证方面的探索，并进一步讨论如何将前沿研究成果融入人工智能安全教学。

简介：白光冬，香港城市大学计算机科学系副教授、博士生导师。北京大学学士（2008）及硕士（2011）学位，新加坡国立大学博士（2015）学位。长期从事可信人工智能、软件工程与形式化方法等领域的研究，在IEEE S&P、NDSS、ICSE、FSE、ASE、POPL、Usenix Security 等顶级会议和IEEE TSE、ACM TOSEM、IEEE TDSC等顶级期刊发表学术论文70余篇。其中，关于大模型应用安全的研究荣获ASE 2024 杰出论文奖。现担任IEEE Transactions on Dependable and Secure Computing（TDSC，CCF-A）、IEEE Transactions on Service Computing（TSC，CCF-A）等期刊副主编。

五、论坛主席简介

1. 论坛主席：邓玉欣 教授

简介：邓玉欣，上海财经大学计算机与人工智能学院教授、CCF杰出会员。主要研究方向包括并发计算模型、程序理论、量子计算。出版专著1本，发表学术论文110余篇，多篇出现在国际权威期刊和会议如Information and Computation、Theoretical Computer Science、ICALP、LICS、POPL等。曾为CONCUR 2018作特邀报告。担任期刊Theoretical Computer Science和Scientific Annuals of Computer Science编委，多次担任 CAV、LICS等会议的程序委员会成员。曾获2024年中国计算机学会自然科学二等奖、SETTA 2024最佳论文奖。已出版《函数式程序设计》、《量子计算导论》两部教材。

2. 论坛主席：李晓红 教授

简介：李晓红，天津大学英才教授、博导，天津市教学名师，从事软件与系统安全、人工智能安全及区块链安全研究。主持和参与国家重点研发、国自然重点30余项，在包括TDSC、TIFS、TSE、TOSEM、ASE、ICSE、FSE、NDSS、IEEE S&P、CCS顶刊顶会发表论文160余篇。两次获ACM SIGSOFT杰出论文奖，指导博士生论文获得CCF优秀博士学位论文，获天津市科技进步一等奖、湖北省科技进步一等奖。获国家级教学成果二等奖、天津教学成果特等奖。指导学生在国际“互联网+”和“挑战杯”竞赛中获得金奖和特等奖。

3. 论坛主席：曹钦翔 副教授

简介：曹钦翔，上海交通大学副教授，长期研究程序验证、程序逻辑与交互式定理证明，并研究人工智能技术在这些领域的应用。他2013年本科毕业于北京大学获得哲学（逻辑与科学哲学）学士学位获得数学双学士学位，于2018年在美国普林斯顿大学获得计算机博士学位。他在程序验证领域的代表性研究成果VST、VST-A验证工具是目前用于验证实际程序功能正确性的最好结果之一，相关成果发表于TOPLAS、POPL、NSDI、OOPSLA、ICFP、JAR等国际一流会议与期刊。2016年的哥德尔奖得主Peter O'Hearn曾评价这些工作“在具有挑战性的程序验证问题中获得了令人印象深刻的成果”。他参与发起了TPChina定理证明开放社区，他目前是中国计算机学会形式化方法专委会的执行委员。