CCF软件大会2026|软件形式化工程方法论坛

一、论坛介绍

软件测试能够揭示程序中存在的错误，而形式验证能够证明程序的正确性。测试作为确认软件功能以及发现程序错误的有效技术, 相对容易进行，但成本可能很高，并且无法确保程序没有错误。相比之下, 形式化验证有可能证明程序的正确性并节省时间，但往往受技术能力限制并需要使用者具备较高的专业知识, 难以推广应用。如何将这两种方法的优势结合起来，同时克服它们的局限性，以实现自动化的软件正确性验证(verification)与妥当性确认(validation)，是一个极具吸引力的科学理论与技术问题, 不仅研究上受到重视, 而且对工业界有巨大的魅力。

二、论坛组织委员会

• 刘少英（华东师范大学）
• 田聪（西安电子科技大学）
• 刘艾（南京航空航天大学）

三、论坛安排

日程安排：

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

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

论坛议程：

四、论坛报告嘉宾简介

1. 报告人：刘少英 教授

题目：Agile-SOFL：敏捷形式化工程方法

摘要：形式化方法为开发正确的软件系统提供了坚实的理论基础和方法，但在实际应用中难以适应大规模软件开发的复杂情况和要求。敏捷开发方法适应软件工程的人主导，大规模，不断演化，以及容易出错的特点，但面临由大量修改软件代码所带来的沉重的工作负担和较高的费用，并难以保障软件的正确性。为了克服形式化方法和敏捷开发方法的这些缺点并发挥其优点，我们提出了Agile-SOFL这个敏捷形式化工程方法。该方法有效地把形式化方法与敏捷开发方法相结合，支持在建立以半形式化规约为主要特点的混合型规约（hybrid specification）的基础上，增量实现软件系统并进行复审和测试的方法。混合型规约以结构化形式定义运算的各种功能场景，但对关键功能的定义使用形式化规约，同时支持用户界面的设计以及描述各种界面之间的关系。书写混合型规约的目的是防止与用户需求有关的错误，并同时为后续的增量实现建立基础。复审技术充分利用混合型规约提高代码复审的质量。测试技术充分发挥规约的作用以提高测试的自动化和效率。Agile-SOFL的目的，是为了提高开发效率和软件质量，但同时也为开发者享受开发过程提供支持。

简介：刘少英，华东师范大学特聘教授，入选教育部长江学者奖励计划, IEEE Fellow, BCS Fellow，AAIS Fellow. 1992年获得英国曼彻斯特大学计算机科学博士学位。曾先后在中国，英国，以及日本的10所大学从事研究和教学工作，主要研究领域包括高可信软件工程，形式化工程方法，软件测试与验证，以及人机结对编程。开创和发展了``形式化工程方法''，设计了SOFL形式化规约描述语言和开发方法，开发了敏捷SOFL形式化工程方法，由Springer出版专著两本，编著由IEEE 和Springer LNCS系列出版的论文集15本，在国际学术期刊和国际会议发表300多篇论文，被邀为15个以上的学术会议作主旨报告，曾获多项学术奖项，担任多个国际会议大会主席和程序委员会主席。

2. 报告人：赵建军 教授

题目：Why Quantum Software Needs Formal Engineering Methods

摘要：Quantum programs are fundamentally different from classical programs. Superposition, entanglement, measurement, and probabilistic behavior make program states difficult to observe and program behavior difficult to reason about in conventional ways. As quantum programs grow into real software, these differences create new challenges for analysis, verification, testing, and debugging. In this talk, I will discuss why quantum software needs formal engineering methods, drawing on our recent work in quantum software engineering. I will show how rigorous reasoning and analysis can help us better understand quantum program behavior and support practical tasks such as program analysis, verification, and testing. More broadly, I will discuss how formal methods and software engineering techniques can work together to make quantum software development more systematic and reliable.

简介：Jianjun Zhao is a Professor at Kyushu University, Japan, whose research spans software engineering, programming languages, and quantum computing. He is interested in a simple question: as quantum programs become real software, how can we reason about them precisely while still supporting practical software development? Building on his long-standing work in program analysis, testing, debugging, and software quality, he now focuses on quantum software engineering, particularly the quality assurance of quantum software. More broadly, his work aims to bring rigorous reasoning and practical software engineering together to make quantum software more systematic and reliable.

3. 报告人：刘杨 教授

题目：知识形式化驱动人工智能

摘要：人工智能的发展正从"规模驱动"逐步迈向"知识与架构驱动"。现有大模型在模式识别和语言生成方面表现突出，但在逻辑推理、长期记忆、抽象归纳、因果分析与自我反思等方面仍存在局限。其根本原因在于，知识尚未被充分转化为可表示、可计算、可验证和可执行的形式。因此，知识形式化不仅是提升人工智能推理能力的关键，也是构建具备认知能力的智能系统的重要基础。本次讲座将围绕"知识形式化驱动人工智能"展开，介绍一套受大脑认知机制启发的自主智能体计算架构。该架构以知识的结构化表达、动态组织与可执行推理为核心，将非结构化信息转化为概念、规则、关系、因果模型、任务流程与经验记忆，并进一步实现知识的获取、巩固、调用、修正和迁移。在此基础上，系统融合逻辑推理、因果推断、记忆管理、元认知与目标导向的问题求解能力，使知识不再只是静态信息，而是能够支撑智能体理解环境、制定计划、执行任务和持续反思的认知基础设施。最后，本次讲座将进一步讨论知识形式化与通用人工智能之间的关系，探索一条融合神经科学、心理学、社会科学与计算机科学的跨学科研究路径。人工智能的未来不仅取决于模型规模的增长，更取决于能否建立统一的知识表示、推理、记忆与行动机制，将人类知识转化为可计算、可组合、可演化的智能底层结构。

简介：刘杨博士现任新加坡南洋理工大学教授、网络安全研究中心执行主任、新加坡网络安全研究办公室执行主任。2019年荣获南洋理工大学大学领袖论坛讲席教授，2024年荣获校长讲席教授。刘杨博士长期专注于软件工程、网络安全与人工智能领域研究，其工作致力于弥合理论与实践之间的鸿沟，利用程序分析、数据分析及人工智能技术，对软件的设计与实现进行高可信与高安全性的评估与优化。他的多项科研成果已实现成功转化和商业化。迄今为止，他已在国际顶级学术会议和期刊上发表论文 500 余篇，并获得 30 项最佳论文奖及 1 项国际软件工程顶会最具影响力系统奖。同时，他领导多家核心研究中心与重点项目，包括南洋理工大学网络安全研发平台、新加坡网络安全研究办公室、南洋理工可信人工智能研究中心(TAICeN)，以及与帝国理工学院（ICL）共建的 CREATE 医疗设备安全联合研究中心。刘杨博士先后斩获多项重磅学术荣誉，包括微软亚洲研究院学者奖、新加坡科技研究局青年学者基金、南洋青年教授基金、陈振传学者基金、南洋科研成就奖、ACM 杰出讲者、新加坡国家研究基金会研究员、南洋理工创新创业先锋奖等。

4. 报告人：马雷 教授

题目：Towards Trustworthiness Assurance of Intelligent Systems in the Agentic AI Era

摘要：Recent advances in data-driven, AI-enabled systems have led to a rapid proliferation of intelligent applications across diverse domains. This growth has been further accelerated by the emergence of large foundation models, which now serve as the backbone of many modern agentic AI systems. However, the increasing complexity and centralization of these models introduce new challenges in ensuring their trustworthiness. In this talk, I will provide a high-level overview of our ongoing exploratory research on the assurance and engineering of trustworthy AI-enabled systems in the era of agentic AI. I will also highlight key challenges and emerging opportunities, both in shaping future research directions and in enabling value transformation in industrial applications.

简介：Lei Ma is currently an Associate Professor with the University of Tokyo and an associate professor with University of Alberta. He is a Canada CIFAR AI Chair and Fellow of Amii - Alberta Machine Intelligence Institute. His research centers around the interdisciplinary fields of human-centered trustworthy artificial intelligence (AI), software engineering (SE) with a special focus on quality, reliability, safety, and security assurance, as well as the interpretation and human interactivity of and AI Systems. Many of his works were published in top-tier software engineering and AI, venues, among which a few received the ACM SIGSOFT Distinguished Paper Awards (ASE 16, ASE 18, ASE 18, FSE 23, ISSTA 2026), an annual best paper award of the 2022 IEEE Transactions on Software Engineering (TSE 2022), and IEEE TCSE New Directions Awards (2025) for his continued community contribution on the direction "Trustworthy assurance for data-driven software systems".

5. 报告人：苏亭 教授

题目：模型引导的功能性质测试技术及其应用

摘要：真实世界中的关键软件系统往往功能逻辑复杂，需要在代码频繁变更情况下，持续保障功能安全可靠和高可用。本报告将介绍近几年我们华东师范大学研究小组正在探索的一种模型引导的功能性质测试技术，该技术的思想是从软件系统的系统需求用例、API接口规范等不同形式的模型出发，并利用该类模型引导实现更高验证强度的功能性质测试，以发现重要软件缺陷。目前该技术在微信支付、集成电路制造等关键场景得到了应用。

简介：华东师范大学软件工程学院教授、副院长（科研），入选国家级青年人才计划，主要研究方向为软件分析、测试、验证与安全，以及工业软件等。相关技术成果形成了商业化软件测试与验证工具或被头部企业工具集成，应用领域涉及集成电路制造、航空航天、金融支付、国产鸿蒙系统等。曾获得CCF科技成果奖技术发明一等奖、CCF青年科技奖（软工和系统专委）、研究成果曾入选 CCF产学合作基金项目成果合集、荣获七项CCF-A类国际会议的ACM SIGSOFT杰出论文奖等；主持中国国自然面上项目、科技部重点研发计划课题、以及企业项目十余项。个人主页：http://tingsu.github.io/。

6. 报告人：林望 教授

题目：基于形式化方法的自主智能系统安全分析与控制

摘要：随着人工智能技术的飞速发展，自主智能系统广泛已应用于航空、航天、医疗、交通等安全攸关领域，其行为正确性至关重要。自主智能系统中信息计算与物理设备的交互特性，以及深度学习赋能的计算范式，给其安全分析与控制带来挑战。本报告将介绍我们在自主智能系统形式化分析与控制方面取得的一些研究成果，包括自治系统安全控制器设计与优化、多智能体系统分布式安全控制等。

简介：林望，浙江理工大学计算机科学与技术学院教授、副院长，智能无人系统可靠性工程浙江省国际科技合作基地副主任，CCF形式化方法专委会、系统软件专委会执行委员。主要研究方向为形式化方法、可信智能系统安全等，主持国家自然科学基金面上项目、浙江省自然科学基金重大项目等，参与国家高性能计算重大专项课题、国家自然科学基金重点项目等，部分成果发表于《中国科学》、IEEE TCAD、CAV、FM、CVPR、EMSOFT、HSCC、DAC、AAAI、IJCAI等相关领域重要期刊与会议。

7. 报告人：曲南江 博士

题目：AIG结构中的并行性与共享性：从逻辑重写到组合等价性检查

摘要：随着数字电路规模和设计复杂度持续增长，以与非图（And-Inverter Graph，AIG）为中间表示的逻辑综合与形式验证面临显著的可扩展性挑战：逻辑重写中的结构依赖限制并行执行，组合等价性检查中的公共逻辑重复编码与SAT任务负载差异又会削弱并行效率。本报告围绕如何利用AIG结构信息提升逻辑重写与等价验证的可扩展性展开。首先，介绍分治并行逻辑重写方法DACPara，通过按层划分、阶段解耦与动态全局信息维护挖掘并行重写机会，在保持功能等价并取得与串行方法相当的优化质量的同时，在40个物理核上相对单线程ABC取得34.36倍平均加速。进一步，介绍基于因式分解形式共享的并行组合等价性检查方法，利用因式分解形式文字数表征公共逻辑及其CNF编码的复用潜力，结合分支复杂度估计SAT任务代价，指导共享感知任务划分与动态映射，在40个物理核上相对同平台单线程ABC取得45.57倍几何平均加速。两项工作分别从挖掘结构并行性和利用结构共享性出发，展示AIG结构信息如何支撑并行逻辑重写、公共逻辑复用与验证任务组织，为大规模数字电路优化与形式验证提供可扩展的实现思路。

简介：曲南江，西安电子科技大学计算机科学与技术学院博士后。主要从事电子设计自动化（EDA）领域的数字电路逻辑综合、形式验证及相关并行算法研究，相关成果发表于或录用于DAC 2024、DAC 2026和ACM TODAES等国际会议和期刊。曾作为参赛项目负责人，获2021年第七届中国国际"互联网+"大学生创新创业大赛全国金奖。

8. 报告人：刘艾 博士

题目：基于测试的形式化验证：方法扩展与验证准则

摘要：基于测试的形式化验证（TBFV）将规约测试与Hoare逻辑相结合，通过确保程序执行路径的正确性来降低测试成本并保障软件可靠性。本报告介绍我们在TBFV上的系列工作。在方法扩展方面，为Java中Vector、ArrayList和LinkedList类构建Hoare公理，使TBFV能处理复杂数据结构与副作用，缺陷检测能力较规约测试显著提升。在切片集成方面，提出功能可靠性与功能完备性概念，将TBFV与程序切片结合，缩减程序规模的同时自动分析这两个维度。在覆盖率优化方面，提出条件序列覆盖率准则及自动测试用例生成算法，确保条件被充分探索，无需预设上限即可自动终止，在缺陷检测与执行效率上均优于随机测试。TBFV方法能够有效发现语义缺陷，在保证严谨性的同时大幅减少测试用例数量，为软件形式化工程提供兼顾自动化与实用性的技术路径。

简介：刘艾，南京航空航天大学计算机科学与技术学院副教授、博导，本科毕业于中国科学技术大学少年班学院，博士毕业于北京大学数学科学学院，曾任日本广岛大学助理教授，国家重大人才工程A类青年人才，CCF形式化方法专委会执行委员，CCF YOCSEF南京学术委员，中国航空学会计算与仿真专委青年委员，研究方向包括基于范畴论的因果推理、软件形式化方法、量子软件的程序演算等。

五、论坛组织委员会简介

1. 论坛组委会：刘少英 教授

简介：刘少英，华东师范大学特聘教授，入选教育部长江学者奖励计划, IEEE Fellow, BCS Fellow，AAIS Fellow. 1992年获得英国曼彻斯特大学计算机科学博士学位。曾先后在中国，英国，以及日本的10所大学从事研究和教学工作，主要研究领域包括高可信软件工程，形式化工程方法，软件测试与验证，以及人机结对编程。开创和发展了``形式化工程方法''，设计了SOFL形式化规约描述语言和开发方法，开发了敏捷SOFL形式化工程方法，由Springer出版专著两本，编著由IEEE 和Springer LNCS系列出版的论文集15本，在国际学术期刊和国际会议发表300多篇论文，被邀为15个以上的学术会议作主旨报告，曾获多项学术奖项，担任多个国际会议大会主席和程序委员会主席。

2. 论坛组委会：田聪 教授

简介：田聪，西安电子科技大学，二级教授，国家级领军人才。长期从事可信软件、形式化验证理论与方法研究，在LICS、CAV、ICSE、FSE、ASE、ISSTA、DAC、TOSEM、TSE、TCAD软件学报等国内外顶级期刊和会议发表论文200余篇；主持国家自然科学基金重大课题、重点和优青项目、科技部重点研发计划课题、军委装备发展部等项目十余项；担任计算机学会形式化方法专委会副主任，获中创软件人才奖、教育部自然科学一等奖1项、陕西省科学技术一等奖2项；相关研究成果应用于航天控制软件开发和芯片设计EDA软件验证等领域。

3. 论坛组委会：刘艾 博士

简介：刘艾，南京航空航天大学副教授、博导，本科毕业于中国科学技术大学少年班学院，博士毕业于北京大学数学科学学院，曾任日本广岛大学助理教授，国家重大人才工程A类青年人才，CCF形式化方法专委会执行委员，CCF YOCSEF南京学术委员，中国航空学会计算与仿真专委青年委员，研究方向包括基于范畴论的因果推理、软件形式化方法、量子软件的程序演算等。