CCF软件大会2026|形式化方法与应用论坛

一、论坛介绍

形式化方法以严格的数学模型和机械化推理为基础，支持计算系统的规约、设计、构建、验证与演进，是保障系统正确性、安全性和可靠性的重要手段。相关方法已应用于芯片设计、软件验证等领域，并逐步拓展至区块链、可信人工智能等新兴领域。与此同时，形式化方法与生成式人工智能的交叉研究不断发展，为自动化建模、程序验证和定理证明带来新的研究方向。

"形式化方法与应用"专刊论坛围绕形式化方法的基础理论、验证技术、支撑工具及领域应用展开，重点关注其与理论计算机科学、程序语言、软件工程、基础软件、电子设计自动化（EDA）、实时嵌入式系统、人机物融合系统、概率与量子系统、网络与信息安全、可信人工智能及生成式人工智能等领域的交叉研究。

本次论坛拟安排10篇论文报告，内容涵盖SMT求解器测试、数学定理与量子纠错码的形式化验证、并发程序与Rust操作系统内核验证、密码分析、混成系统定理证明、统计模型检验及神经网络控制系统安全。论坛为相关领域研究人员提供交流平台，分享理论、方法、工具和应用方面的研究进展，促进形式化方法在实际系统中的应用。

二、论坛组织委员会

• 陈宇奇（上海科技大学）
• 李国强（上海交通大学）
• 田聪（西安电子科技大学）

三、论坛安排

日程安排：

时间：2026年11月8日,9:00-12:00

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

论坛议程：

四、论坛报告嘉宾简介

1. 报告人：孙茂林（博士研究生）

题目：SMT求解器测试:问题、进展与挑战

摘要：SMT求解器的正确性与可靠性直接影响程序验证、符号执行和漏洞分析的结论。本报告围绕有效测试输入生成、缺乏通用测试预言以及有限资源下的搜索效率等挑战，系统梳理求解器测试的研究进展，比较差分测试、蜕变测试、已知结果构造和输出验证等机制的适用条件，并讨论运行时与资源消耗异常的确认方法。在此基础上，介绍机制比较框架、评价影响因素模型及标准化报告规范，结合版本回归、状态化API、下游查询稳定性和性能退化检测等场景，给出方法选择与配置建议。

简介：孙茂林，南京大学计算机学院博士研究生，师从杨已彪研究员和周毓明教授，隶属徐宝文教授团队。主要研究方向为软件分析与测试，重点关注约束求解器与编译工具链的缺陷检测，以及大语言模型辅助的软件质量保障。已在ASPLOS、OOPSLA、ICSE、FSE、ISSTA、TOSEM、TSE等CCF-A类会议和期刊发表论文20余篇，其中以第一作者身份发表8篇，并曾获ACM SIGSOFT Distinguished Paper Award（ISSTA 2026）。在GCC、LLVM、Z3等开源基础软件中累计报告缺陷600余个。主持国家自然科学基金青年学生基础研究项目，入选中国科协青年科技人才培育工程博士生专项计划。

2. 报告人：白子卉（博士研究生）

题目：广义加权Pólya枚举的Lean 4形式化及其应用

摘要：对称枚举通过群作用的轨道与固定点分析计算本质不同的构型。本报告介绍广义加权Pólya枚举在Lean 4中的形式化：建立带权有限和的轨道重索引与逐循环权重分解，构造位置与颜色联合作用下的固定点表示，并将这些构造组织为可复用接口。研究形式化证明任意有限群作用下的一般加权Burnside定理，推导加权Pólya公式，以及乘积置换群任意有限子群下的无权与加权de Bruijn型闭式。最后展示六珠二元手链、立方体染色和简单图同构类等实例的机器验证。

简介：白子卉，女，华东师范大学软件工程学院博士研究生，导师为杨争峰教授。主要研究方向为形式化方法与符号计算。

3. 报告人：贺腾宇（硕士研究生）

题目：纠缠辅助量子纠错码对偶定理形式化验证

摘要：纠缠辅助量子纠错码的对偶理论揭示原码与对偶码在编码参数、稳定子结构及最小距离上的关系，但传统推导中的前提条件与表示转换缺乏系统检查。本报告介绍基于Lean 4、Mathlib和QECLean的形式化验证工作，分别证明对偶定理的二元辛表示与四元加性码表示，验证稳定子与正规化子作用的交换关系，并刻画原码及其对偶码的最小距离。通过典型实例的机器检查，为对偶理论及相关构造提供可检查的数学正确性保证。

简介：贺腾宇，现为首都师范大学信息工程学院在读研究生。主要研究方向为定理证明与形式化数学，关注利用 Lean 定理证明器对数学理论进行形式化建模与证明。目前以量子纠错码理论为研究对象，开展纠缠辅助量子纠错码的构造、对偶关系及距离性质的形式化证明，并探索不同数学表示之间的证明复用。希望与同行交流定理证明方法及其在量子信息领域的应用。

4. 报告人：王超（副教授）

题目：单调可线性化及其形式化验证研究

摘要：复杂的可线性化点机制增加了并发对象验证的难度。本报告介绍一种基于确认点思想的新一致性——单调可线性化，要求随着执行推进，可线性化序列的操作集合保持不变或单调递增。研究证明其严格强于可线性化、严格弱于决断可线性化，并给出基于前向模拟关系的完备验证方法：由顺序规约构造相应并发对象，将单调可线性化判定归结为操作语义间的前向模拟。最后介绍在Isabelle/HOL中的建模与证明，以及对采用不同可线性化点机制的八个并发对象的验证。

简介：王超，博士，西南大学计算机与信息科学学院/软件学院副教授，获中国科学院软件研究所博士学位。主要研究方向为形式化方法，重点研究并发对象与分布式数据类型的一致性理论及形式化验证。在PLDI、CONCUR等国际学术会议和《中国科学：信息科学》《软件学报》、Acta Informatica等学术期刊上发表多篇论文，主持国家自然科学基金青年科学基金项目。

5. 报告人：万新熠（助理研究员）

题目：Rust通用操作系统内核基础库OSTD的形式化验证

摘要：通用操作系统内核的形式化验证成本较高。本报告介绍利用Rust的safe/unsafe边界缩小验证范围的方法，并以Verus对内核基础库OSTD的关键组件进行验证。研究建立统一的全局逻辑状态与资源不变式，描述运行时对象、逻辑权限及资源生命周期之间的关系；通过细粒度状态机与原子抽象状态机的前向模拟，证明页表Cursor创建过程的逻辑原子性；针对读写锁等同步原语，验证权限获取、升级与释放过程中的正确转移。该工作为实际内核的unsafe基础层及上层safe Rust服务提供内存安全基础。

简介：万新熠，蚂蚁技术研究院助理研究员，毕业于上海交通大学，主要从事Rust语言与操作系统形式化验证相关研究。目前负责Rust框内核操作系统星绽（Asterinas）的形式化验证工作，致力于利用形式化方法提升操作系统内核的安全性与可靠性，探索形式化验证技术在实际系统软件中的应用。

6. 报告人：贾凤鸣（硕士研究生）

题目：基于EasyBC的SPN结构分组密码自动化截断差分分析

摘要：本报告面向线性扩散层可分解为局部列混合操作的字级SPN分组密码，介绍基于EasyBC的统一截断差分自动化分析流程，以及混合整数线性规划和布尔逻辑两种建模方法。研究使用分支特性表描述传播概率，通过可调精度离散化与MaxSMT构造概率负对数的布尔逻辑表示，并比较伪布尔约束的CNF转换方法及三种外层搜索策略。在Midori64、SKINNY64、CRAFT、RAIN64和LED64上的实验显示，两种建模方法在相同离散化精度下结论一致、效率互补；二分搜索具有较好的综合稳定性。

简介：贾凤鸣，中国科学院大学软件工程专业硕士研究生，现于中国科学院软件研究所基础软件与系统重点实验室开展科研工作。主要研究方向为形式化方法与分组密码自动化安全分析。目前主要研究基于EasyBC的分组密码自动化截断差分分析方法，关注混合整数线性规划（MILP）、布尔可满足性求解（SAT）等约束求解技术在密码安全性分析中的应用，以及差分传播概率建模与自动化搜索方法。

7. 报告人：金翔宇（博士后）

题目：基于轨迹的组合式混成霍尔逻辑定理证明器

摘要：混成通信顺序进程HCSP及混成霍尔逻辑HHL为混成系统的建模与演绎验证提供理论基础。本报告介绍基于轨迹的组合式HHL交互式定理证明器：在Isabelle/HOL中实现与轨迹语义相匹配的证明系统，并机器证明HHL规则的可靠性、相对完备性等性质。研究进一步实现辅助模块，以简化证明任务、提高证明复用性并增强复杂HCSP模型的验证能力。案例覆盖通信、连续演化、循环和并行组合等行为，展示组合式推理在典型混成系统验证中的应用。

简介：金翔宇，中国科学院软件研究所博士后，2025年毕业于中国科学院大学软件研究所，获得软件工程专业博士学位。主要从事混成系统形式化验证研究，围绕混成通信顺序进程、混成霍尔逻辑及定理证明开展工作，研究并行系统的组合验证与自动化推理方法，开发交互式定理证明器和自动验证工具。

8. 报告人：唐晓辰（博士研究生）

题目：人机物融合自动机切换策略的统计模型检验

摘要：人机物融合自动机HCPA通过在关键状态选择人类或机器控制支持协同控制，但切换策略的存在性结论并不直接保证强化学习得到的具体策略。本报告介绍面向固定切换策略的统计模型检验框架：基于黑盒系统的独立执行样本，比较切换控制与人类、机器单独控制的性质满足概率，分析关键状态切换决策的作用，并在减少低影响切换后重新验证闭环控制。框架给出具有概率近似正确PAC语义的统计结论；Grid-World与Lunar-Lander案例展示了验证具体策略概率优势及减少实际切换次数的效果。

简介：唐晓辰，同济大学软件工程专业博士研究生，导师为张苗苗研究员，主要研究方向为形式化方法、人机物融合系统、强化学习及策略综合，目前已在CCF-A类会议RTSS、CCF-B类期刊Journal of Systems Architecture等国际学术会议和期刊发表多篇学术论文，研究工作聚焦于人机物融合系统的模型定义以及基于强化学习的策略综合。

9. 报告人：何嘉骐（软件工程专业直博生）

题目：基于扩散模型的视觉控制系统概率安全验证

摘要：高维视觉感知与环境不确定性使视觉神经网络控制系统的安全验证面临挑战。本报告介绍基于条件扩散模型的概率安全验证框架，学习系统状态与环境条件共同作用下的视觉观测分布，以刻画感知不确定性。框架进一步构建用于验证的随机微分方程闭环系统，将感知不确定性经视觉强化学习策略传播至状态空间随机动力学，并结合神经网络障碍证书综合，获得无限时间范围内系统安全概率的可证明下界。最后介绍真实视觉控制任务上的实验结果及方法有效性。

简介：何嘉骐，中国人民解放军国防科技大学计算机学院软件工程专业直博生，主要研究方向为视觉感知驱动的强化学习控制与智能控制系统安全性验证。研究聚焦复杂动态环境下自主系统的感知、决策与控制问题，探索视觉信息与强化学习算法的深度融合，研究面向环境不确定性的智能控制策略优化与安全保障方法。同时，结合形式化方法与安全性验证技术，探索智能控制系统运行行为的分析与验证机制，为提升无人系统在复杂场景下的自主决策能力、运行可靠性与安全保障水平提供技术支撑。

10. 报告人：王培新（青年研究员）

题目：基于障碍证书的神经网络控制系统运行时安全防护方法

摘要：神经网络控制系统在运行时可能受到环境扰动，真实状态难以准确获知。本报告介绍基于障碍证书的运行时安全防护方法：构造覆盖实际状态及其扰动状态的过近似集合，将安全判定转化为障碍证书约束满足问题，以保证验证结果的正确性；将不安全动作的修正建模为受约束的二分搜索，在安全约束下快速寻找可执行动作。安全任务与可达—避障任务上的实验表明，该方法在所测试的不同状态扰动条件下均保持系统安全，兼顾安全判定的正确性与运行时求解效率。

简介：王培新，华东师范大学软件工程学院青年研究员、博士生导师，曾在新加坡南洋理工大学和英国牛津大学担任博士后研究员。主要研究方向包括可信人工智能、程序语言与形式化方法，重点关注复杂场景下智能软件系统的安全性与可信性。相关成果发表于 POPL、PLDI、OOPSLA、CAV、FM、NeurIPS、ICLR等国际顶级会议和期刊。

五、论坛组织委员会简介

1. 陈宇奇 上海科技大学 助理教授、研究员

简介：陈宇奇，博士，上海科技大学信息科学与技术学院助理教授、研究员。研究方向包括形式化方法、系统安全、软件工程和程序语言，关注人工智能系统安全，以及程序分析、形式化验证和测试技术。在NDSS、IEEE S&P、FSE、ISSTA、ASE等会议发表研究成果，担任IEEE TSE、ACM TOSEM、IEEE TC等期刊审稿人及相关会议程序委员会成员。主持国家自然科学基金、上海市科委等科研项目。

2. 李国强 上海交通大学 副教授

简介：李国强，博士，上海交通大学计算机学院副教授、博士生导师，中国计算机学会高级会员。研究方向包括形式化验证、程序语言理论、程序智能及零知识证明。主持国家自然科学基金五项、重点项目子课题两项，在OOPSLA、FM、ASE、FSE、ICSE等会议及TSE、TDSC、TECS等期刊发表论文。现任中国计算机学会形式化方法专委会常务委员、上海计算机学会理论计算机科学专委会副主任。

3. 田聪 西安电子科技大学 教授

简介：田聪，博士，西安电子科技大学计算机科学与技术学院二级教授、博士生导师，国家级领军人才。长期从事可信软件、形式化验证理论与方法研究，研究方向包括AI与可信软件、量子计算和具身智能。主持国家自然科学基金重大课题、重点和优青项目等科研项目，担任中国计算机学会形式化方法专委会副主任。获中创软件人才奖、教育部自然科学一等奖及陕西省科学技术一等奖，相关成果应用于航天控制软件开发和芯片设计EDA软件验证等领域。