CCF软件大会2026|约束求解技术与应用论坛

一、论坛介绍

"约束求解"，一般是指一种方法论——强调对问题通过某种数学语言进行形式化表达，然后对其进行求解，是计算机解决问题的一种常见方法论。约束求解根植于计算机科学中的基础问题，尤其，逻辑公式可满足性问题是理论计算机和数理逻辑领域的核心问题。同时，约束求解器是软硬件验证与测试的基础引擎，是工业软件的核心部件，是密码分析的重要工具，在多个关键行业具有广泛应用，对国家经济和社会发展起着至关重要的作用。

经过长期发展，约束求解技术已取得显著进步，并在软硬件验证、信息安全及各类工业智能决策等场景中取得了一系列成功应用。然而，在将这些技术真正落地到实际业务场景的过程中，却日益凸显出技术与应用之间的明显脱节。尽管已有不少求解方法与工具被开发出来，但在面对真实问题的复杂度、规模以及实时性等实际需求时，往往出现适配困难、表现不稳的"落地鸿沟"。尤其在诸多关键领域，现有求解技术仍难以应对具有挑战性的实际实例，无法满足现实场景对可靠性、扩展性与适用性的综合要求，亟需在技术向应用转化上实现有效突破。

约束求解学术论坛拟围绕基础理论突破、核心技术攻坚、产业应用创新以及未来技术发展等方面展开深入探讨，本次论坛拟邀请各领域顶级专家学者，就约束的理论研究、求解算法以及行业应用实践等多个方向进行交流，分享相关研究观点、成功案例与技术挑战，探讨如何发展约束求解的理论研究、提高求解效率并提升算法扩展性。欢迎计算机科学、应用数学、运筹学、优化理论等相关学科专家和学者前来参加。

二、论坛组织委员会

• 罗川（北京航空航天大学）
• 姚培森（浙江大学）
• 马菲菲（中国科学院软件研究所）

三、论坛安排

日程安排：

时间：2026年11月7日，15:20~18:20

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

论坛议程：

四、论坛报告嘉宾简介

1. 报告人：张健 中国科学院软件研究所研究员

题目：约束求解研究概览

摘要：约束满足问题是一个通用的问题求解框架。约束求解技术和工具可以应用于很多领域，包括：运筹规划和调度，软件分析与验证，硬件设计自动化，密码分析，数学问题求解，等等。本报告将结合具体应用，介绍约束的多种形式、约束求解的基本技术及若干工具、近期的部分研究进展；也将涉及一些相近的其他问题。

简介：张健，中国科学院软件研究所研究员，中国科学院大学岗位教授。CCF会士、监事。主要研究兴趣包括：软件测试与分析、自动推理、约束求解等。曾主持国家杰出青年科学基金、国家973计划等项目。曾获中创软件人才奖、国务院政府特殊津贴、CCF科技成果奖自然科学一等奖。担任《计算机学报》，Journal of Computer Science and Technology，Frontiers of Computer Science，《计算机科学与探索》等期刊编委。

2. 报告人：蔡少伟 中国科学院软件研究所/北京航空航天大学 研究员

题目：大模型辅助的约束求解：算法理论与求解器

摘要：命题逻辑可满足性（SAT）和可满足性模理论（SMT）问题是形式化方法的基础引擎，其理论和工程研究都广受关注。近年来，大语言模型在理论分析和算法研发方面展现了优秀的能力，为SAT和SMT研究提供了新思路。利用大模型技术，我们得到了3-SAT问题最好的理论复杂度上界，提高了前沿SAT求解器和SMT求解器的性能，并且解决了一个密码学开放问题。

简介：蔡少伟，中国科学院软件研究所研究员，主要研究约束求解和硬件验证，主持国家自然科学基金重点项目和青年基金B类项目，获得领域顶级会议CAV、CP和SAT的最佳论文奖/杰出论文奖，多次获得国际SAT比赛和SMT比赛冠军，混合整数规划比赛MIPcc亚军。其求解器被集成到英伟达、微软、英特尔、华为、华大九天等公司的软件中，应用于EDA、处理器验证、操作系统验证、以及密码分析。担任SAT 2027会议程序委员会主席，曾在FMCAD、CP和SOCS等国际会议做特邀报告。

3. 报告人：贺飞 清华大学副教授

题目：面向并发程序验证的SMT理论及其扩展

摘要：并发是现代软件系统的核心特征。并发在提升性能的同时，也带来共享访问冲突与弱内存一致性等问题，使程序更难构建且更易出错。本报告介绍面向并发程序验证的 SMT 理论，重点阐述如何通过内存操作之间的序关系及其一致性约束，对并发程序行为进行建模与自动推理。在此基础上，进一步介绍该理论向死锁检测和数据竞争检测的最新扩展工作。

简介：贺飞，清华大学长聘副教授、博士生导师，软件系统与工程研究所所长。长期从事程序验证、模型检验与自动推理研究，在程序终止性证明、并发程序验证及面向验证的SMT理论方面取得成果。开发的并发程序验证工具四次获国际软件验证大赛并发安全赛道冠军。发表论文百余篇，入选国家特支计划青年人才，获"中创软件人才奖"。

4. 报告人：钱超 南京大学教授

题目：演化学习：迈向高效通用黑盒优化

摘要：黑盒优化广泛应用于工业制造与自然科学领域，但其求解极具挑战。人工智能领域中，受达尔文进化论启发的演化算法是求解黑盒优化问题的常用方法，却存在求解效率偏低、理论支撑不足等局限。演化学习融合演化算法与机器学习，旨在提升黑盒优化的求解能力。本报告将介绍我们围绕构建演化学习理论基础开展的系列研究，阐述在理论成果指导下设计的算法，如何攻克芯片布局这一工业 "卡脖子" 难题，并探索生命起源与演化这类自然科学基础问题。最后，将介绍面向高效通用黑盒优化，我们在黑盒优化智能体方向的相关探索。

简介：钱超，南京大学人工智能学院教授，新一代人工智能国家科技重大专项负责人。长期从事人工智能中演化学习基础理论研究，出版《演化学习》等中英文著作2部，以第一/通讯作者在人工智能顶级期刊/会议发表论文70余篇，获ACM GECCO'11最佳理论论文奖，成果被国家自然科学基金委官网报道。理论指导下设计的算法应用于生命起源等自然科学基础问题，成果以共同第一/通讯作者发表于美国国家科学院院刊《PNAS》、《自然-通讯》，入选"2024年中国生态环境十大科技进展"；应用于"卡脖子问题"—芯片布局，获ACM Humies Award、芯片设计顶会DATE'25最佳论文奖；多项技术在华为落地应用，包括芯片布局、芯片寄存器寻优、半导体光路优化等任务，获5次华为"难题揭榜"火花奖(全国第二)。受邀担任IEEE计算智能学会工作组主席，人工智能权威国际期刊AIJ、ECJ、IEEE TEC等编委，在国际人工智能联合大会IJCAI'22作青年成就亮点报告，担任亚太人工智能国际会议PRICAI'25程序主席，获CCF-IEEE CS青年科学家奖。

5. 报告人：史建琦 上海丰蕾信息科技有限公司创始人

题目：特定领域场景下Tensor加速器驱动的SAT/SMT求解

摘要：软件漏洞挖掘、嵌入式固件符号执行、密码算法实现验证，以及协议解析器和 CRC 完整性检查，都依赖 SMT 求解器处理大量路径条件与 XOR/线性约束。报告介绍丰蕾科技Tensor-SMT 如何识别其中的矩阵结构，在保持精确语义的前提下加速适用查询，并对不适用查询安全回退。业务上，可将其接入 angr、自动化测试或形式化验证平台：前端按原流程生成约束，后端自动选择矩阵路径；在 CI、模糊测试、固件发布门禁和安全审计中减少求解等待，同时保留模型校验、超时与回退记录。

简介：史建琦，上海丰蕾信息科技有限公司创始人、董事长、总经理。博士生导师、国家可信嵌入式软件工程技术研究中心、软硬件协同设计技术与应用教育部工程研究中心副主任； 2020年上海市科技进步特等奖获得者、2018年上海市"启明星"科技人才、入选2025年上海市东方英才计划（青年），工业控制软件领域国标委TC124/SC5委员，PLCOpen国际标准组织中国区理事。长期从事可信软件理论与技术、高可信工业控制软件分析与形式化验证、嵌入式实时操作系统验证、系统底层程序分析与验证等方向研究及安全攸关控制系统形式化验证工作。主持国家级、省部级科研项目 20 余项；主导研发的多个产品入选上海市首版次软件、上海市工业软件推荐目录、上海市创新产品推荐目录，SMAVE 系列产品通过 TÜV 南德意志集团安全攸关软件工具开发最高等级认证，覆盖轨道交通、汽车电子、核电及工业控制等行业。

6. 报告人：刘晟材 南方科技大学副研究员

题目：自动算法设计：算法空间蒸馏与代码生成

摘要：优化算法的自动设计，既需要在庞大的算法空间中发现有效算法，也需要使这些算法适应不同的问题实例。算法空间可以由神经网络、参数化求解器乃至可执行代码组成，其表示方式与探索机制直接影响自动设计的效率和效果。本报告将围绕算法空间的组织与探索，介绍两方面研究。首先，从算法空间蒸馏的视角，讨论如何在有限评测信息下构建小规模、互补且可适配的算法字典，实现跨问题类别或跨实例的经验复用。随后，将视角转向代码空间，探索前沿 AI 模型在算法代码生成上的能力边界。

简介：刘晟材，南方科技大学计算机系副研究员、博导，北京中关村学院兼职博导，曾在新加坡科技研究局担任高级研究科学家。长期从事学习优化 (Learn to optimize)、大模型/智能体后训练、AI与量子计算交叉方向的研究，已获批主持国自然基金一项、华为合作项目两项，迄今已在CCF-A类会议以及IEEE TPAMI、TEVC上以一作/通讯作者发表论文30篇。

五、论坛组织委员会简介

1. 论坛组委会：罗川 教授（北京航空航天大学）

简介：罗川，北京航空航天大学教授，博士研究生导师，国家自然科学基金青年科学基金项目（B类）负责人，北航软件学院院长助理、关键基础软件所副所长。围绕约束求解研究方向，开展了一系列创新的学术研究工作。已入选中国科协青年人才托举工程。总计发表CCF-A类论文超过40篇。担任多个国际学术会议的领域主席、（资深）程序委员会成员。作为负责人主持多项国家级科研项目，包括国家科技重大专项课题、国家重点研发计划课题、国家自然科学基金项目等。在国际知名约束求解竞赛中多次获得冠军，包括来自亚洲参赛者的首个冠军。研究工作获得国际知名学者（包括诺贝尔奖得主）实际使用或正面评价。研究成果被国家电网、航天科工集团、华为、微软成功应用，有效提升了云系统、编译器、体系设计软件等关键系统软件的性能和可靠性。

2. 论坛组委会：姚培森 研究员（浙江大学）

简介：姚培森，浙江大学"百人计划"研究员，博士生导师，CCF 形式化方法专委会、理论计算机科学专委会执行委员，ACM SIGPLAN、SIGSAC 会员。主要研究方向为程序分析与验证、程序合成与优化、逻辑与自动推理。相关成果发表于编程语言(PLDI、OOPSLA、ECOOP)、形式化方法(CAV)、计算机系统(ASPLOS)、软件工程(ICSE、FSE、ISSTA、ASE、TOSEM)、信息安全(S&P、USENIX Security、TDSC)等领域的顶级会议与期刊，曾获ACM SIGPLAN杰出论文奖、SIGSOFT杰出论文奖等奖项，并入选国家级青年人才计划。在最优抽象解释、路径敏感分析、稀疏值流分析等方向提出系列优化算法，应用于大规模真实软件的缺陷检测与性能优化，累计获得百余CVE编号。担任POPL、PLDI、OOPSLA、FSE、ISSTA、ASE、CCS等领域顶级会议程序委员会委员，以及 TOPLAS、TOSEM、TSE、TDSC 等期刊审稿人。

3. 论坛组委会：马菲菲 研究员（中国科学院软件研究所）

简介：马菲菲，中国科学院软件研究所研究员，博导，中国科学院大学岗位教授。研究方向为自动推理和约束求解，在IJCAR、ISSAC、CP、SAT、TCS、IJCAI、AAAI、JAIR、NeurIPS、ICCV、EMNLP、ISSTA、ASE等国际高水平会议或期刊上发表论文30余篇。曾获中国科学院青年创新促进会优秀会员，ACM SIGSOFT杰出论文奖，省部级一等奖一项，省部级二等奖一项。