摘要：CCF-华为胡杨林基金由CCF与华为联合发起，旨在通过搭建产学合作平台，连接产业实践问题与学术科研问题，支持海内外优秀青年学者开展与产业结合的前沿科研工作。目前已经覆盖数据库、形式化方法、高性能计算、系统软件、软件工程等多个领域。
2025年度CCF-华为胡杨林基金形式化专项申报截止时间还剩7天，请意向申报学者尽快提交申报表。
2025年度CCF-华为胡杨林基金形式化专项
CCF-华为胡杨林基金
CCF-华为胡杨林基金由CCF与华为联合发起，旨在通过搭建产学合作平台，连接产业实践问题与学术科研问题，支持海内外优秀青年学者开展与产业结合的前沿科研工作。目前已经覆盖数据库、形式化方法、高性能计算、系统软件、软件工程等多个领域。
CCF-华为胡杨林基金形式化专项的主要目标为支持国内形式化方法的提升与竞争力构建，促进学术界与产业界合作、技术成果转化。
本年度申报课题分为两类：开放课题和产业课题。
1.开放课题：不限定具体研究内容，主要资助具有前瞻性、前沿性、能为产业全面升级储备能力，实现关键基础技术底座自主、领先的相关课题，最高资助额度不超过15万。
2.产业课题：主要针对产业典型问题，持续提升形式化技术的能力上界、降低业界应用相关技术的门槛和成本，创造产业价值，形成本基金的正循环，最高资助额度不超过50万。
本年度拟资助的6个产业课题方向：
1、基于大模型的可形式化证明代码生成
2、面向形式化验证的RUST通用借用演算中间语言技术
3、基于TLA+模型的设计与代码功能一致性检查技术
4、面向TypeScript语言的轻量级形式化分析
5、面向大规模代码的神经符号融合分析
6、AI增强大规模 Trace的预测分析技术
课题详情
方向1:基于大模型的可形式化证明代码生成
课题背景
大模型(如GPT-4、Codex、AlphaCode等)，代码生成能力显著增强。公司及业界也在积极推动在更多场景使用大模型生成代码，每年AI生成代码占公司总代码的比重都在大幅增加，预期能达到60%。但AI生成代码在可信度与正确性方面面临非常大的挑战。面对数量庞大的AI代码传统测试方法提供的保障有限，而形式化验证虽能提供数学证明，但适用规模小、过程复杂耗时、且需要高度专业知识。为了避免走“先污染后治理”的老路，我们希望能研究在生成代码的同时生成对应验证规约的技术，让两者互相促进、既能提升代码的正确性、又能提升代码的可验证性。
项目价值：
我们希望基于大模型的可证明代码生成能调和代码生成难度和证明难度。寻找可降低证明难度的代码书写方法，并同时给出证明规约。
由于大模型在生成代码时使用者已经给出了充分的描述，我们期望能根据这些描述整理待验性质，进行自动化验证。
研究内容
探索以下两类路径：
1、基于AI模型的可证明代码生成：探索一套代码生成Agent，能基于SOTA模型和符号工具完成代码生成任务，且能同时生成代码对应的规约。在不损害代码生成性能的同时提升验证成功率。基于上述代码-规约生成Agent构建从SFT到RL的训练方案，训练端到端代码-规约生成大模型，进一步提升验证成功率。
2、基于中间语言的可证明代码生成：基于规约描述生成中间语言，比如Dafny，在中间语言上完成验证，并基于形式化方法将中间语言转换成后端语言。
课题提供
•利用开源测试数据集(MBPP、MathQA-Python、HumanEval、xCodeEval)；
年度目标
•（必选）在基础数据集(MBPP、MathQA-Python)上，生成成功率80%，生成正确率100%；
•（优选）在挑战数据集上(HumanEval，xCodeEval)，生成成功率40%，生成正确率100%。
方向2:面向形式化验证的RUST通用借用演算中间语言技术
课题背景
Rust 语言以其独特的所有权与借用机制实现了高度安全的内存管理语义，然而这也导致其语言语义极为复杂，给静态分析与形式化验证带来了显著挑战。Rust 编译器内部的中间表示（如 MIR）虽具有完备性，但其结构高度工程化、耦合度高、缺乏模块化语义抽象，难以直接服务于形式化建模和推理。
Charon 项目提出了一种基于“借用演算”(Borrow Calculus)建模的中间语言 LLBC(Low-Level Borrow Calculus)，在为验证提供桥梁方面开辟了可行路径。然而其当前语言特性支持仅覆盖Rust的子集，尚未能表达泛型展开、trait语义、闭包、宏生成结构等复杂语言特性，且其语言形式本身也尚未形成稳定、完备的验证友好语义层。
项目价值：
随着Rust编程语言在工业界关注度的持续提升，围绕其开展的形式化验证工具研发愈发重要。但目前没有合适的面向形式化的中间语言，使得相关技术构建面临诸多困难。我们期望通过LLBC的完善，构建一套覆盖全特性的、简洁而结构化的面向形式化验证的Rust中间语言。
研究内容
•本课题拟基于Charon项目的初步成果，系统化地设计一套面向形式化验证的Rust 通用借用演算中间语言（LLBC）技术体系，研究内容包括：
•语言扩展设计：扩展LLBC的语法与语义能力，引入对泛型单态化、Associated Type计算、泛型约束分发等语言特性的建模能力，且有足够强的表达及扩展能力能应对Rust未来更新；
•语义无损抽象建模：构建统一的类型系统模型，整合所有权、生命周期、别名及可变性等核心机制，形成可验证的操作语义框架，实现向单态化LLBC的结构转换；
•规约语言转换机制：定义函数级、数据（类型）级与语句级规约语句的语法结构及解析机制，满足形式化验证需求，重点参考ACSL技术标准、Prusti验证框架及HIP/SLEEK规约语言规范体系。
课题提供
无
年度目标
•（必选）构建一套能覆盖Rust 1.86.0语义、验证导向的LLBC中间语言核心规范；
•（必选）实现一套支持Rust 1.86.0到LLBC的单态化翻译原型工具，以能完整转化 1.86.0 标准库为验收标准；
•（必选）设计兼容霍尔逻辑与分离逻辑的形式化规约语言框架，确保其可在LLBC抽象语法树（AST）中实现规范化表达。
方向3:基于TLA⁺ 模型的设计与代码功能一致性检查技术
课题背景
在复杂系统开发中，验证最终实现严格符合设计规约始终是一项关键而困难的挑战。一方面，传统测试方法依赖人工构造用例，覆盖范围有限，难以捕捉系统状态空间中的深层次缺陷；另一方面，形式化验证虽然理论上能够提供完备保障，但验证实施成本过高。
基于性质的测试(Property-Based Testing，PBT)作为一种介于测试与验证之间的轻量级形式化方法，已逐渐在工业实践中展现出良好前景。该方法通过将形式化模型作为参考标准，生成覆盖性强的行为轨迹或测试用例，检测实际系统行为是否与模型规约一致。这种方式在保留形式化精度的同时，兼顾工程效率与可落地性。
本课题以TLA⁺作为核心建模语言，依托其在并发状态建模、时序性质描述与模型检验方面的优势，融合PBT的工程可行性，拟构建一套系统性的设计-实现一致性检测技术体系，实现从形式化模型到实现验证的闭环支持。
项目价值：
利用TLA⁺模型的状态空间探索能力自动生成高覆盖性测试用例，克服人工构造用例的局限，显著提升对深层次、并发类缺陷的发现能力，减少缺陷逃逸；作为一种相对轻量级的技术方案，将形式化验证的严谨性引入实际开发流程，降低形式化方法的应用门槛和成本，实现“形式化精度”与“工程效率”的平衡。
研究内容：
本课题将围绕TLA⁺ 模型与系统实现之间的一致性检查展开研究，主要包括以下两个方向：
1.TLA⁺ 模型驱动的测试用例生成与行为一致性验证技术
•基于 TLA⁺ 模型自动生成状态迁移轨迹，自动化构造测试用例；
•利用大语言模型辅助建立模型动作与系统接口的语义映射关系，实现测试用例自动绑定与执行；
•支持自动对比系统运行与形式化模型轨迹，判断目标系统在测试用例执行后的实际输出是否与TLA⁺模型轨迹的预期输出一致，实现行为一致性验证。
2.面向并发与分布式系统的轨迹控制与性质检测技术
•基于 TLA⁺ 模型构建并发执行场景下的轨迹集合，生成关键交错执行路径；
•构建线程交错与事件调度控制机制，控制目标系统执行TLA+轨迹等价的并发行为；
•支持死锁、活性、功能安全性等关键并发性质的轨迹级别检测与分析。
课题提供
待验证系统可从已广泛落地应用、具备一定规模的开源并发系统中选取，本课题不额外提供待验证系统的源码或设计文档。
年度目标
•（必选）构建TLA⁺模型驱动的自动化测试工具原型，基于TLA+轨迹自动生成测试用例，初步实现模型与系统接口的语义映射机制，支持用例自动执行，自动比对模型与用例运行结果是否一致；
•（必选）在典型并发系统中实现基于轨迹的并发性质检测框架，在实际系统上验证其精准控制系统并发交错、有效发现深层次并发缺陷的能力。
方向4:面向TypeScript语言的轻量级形式化分析
课题背景
随着TypeScript在前端、后端以及跨平台应用（尤其是ArkTS在鸿蒙生态中的兴起）中的广泛应用，影响其代码的健壮性和可靠性问题（如：内存泄漏、非法访问等内存类问题等）变得至关重要。轻量级形式化分析作为一种在开发早期阶段发现潜在缺陷的技术，正逐渐受到重视。然而，在TypeScript及其相关生态中推广和应用轻量级形式化分析，仍面临诸多难题。
TypeScript虽然引入了静态类型系统，但为了与JavaScript兼容，仍然保留了许多动态特性，这为应用形式化技术自动化保障代码健壮性带来了复杂性。尤其涉及框架、ETS语言扩展、ABI交互的环境下，利用形式化技术建模分析的难度陡增。目前针对JavaScript/TypeScript的静态检查工具(如ESLint、TSLint的某些插件、SonarQube等)更多侧重于代码风格、基本错误检查和部分已知简单漏洞模式匹配，对于深层次的内存错误、并发问题、分析复杂依赖等方面的形式化验证能力有限。
项目价值：
本课题的研究对于提升TypeScript的Web、移动端和后端应用程序内存管理和稳定性具有重要意义，能够为广泛的Web应用/微服务/鸿蒙操作系统等领域提供可靠的技术支持和形式化保障。通过开发高效形式化分析工具，将带来显著的价值：
1.提升软件质量与可靠性：
•缺陷早期发现：在编码阶段甚至更早发现深层次的逻辑错误、类型不匹配、并发问题和资源泄漏等，降低后期修复成本；
•减少运行时崩溃：通过静态分析消除潜在的运行时异常，提升应用的稳定性和用户体验；
•提升软件性能：通过形式化分析减少系统崩溃和资源浪费问题，从而为大规模软件系统的安全和可靠性提供保障。
2.降低开发与维护成本：
•降低测试成本：精确的问题定位能显著减少开发者在测试与调试上花费的时间；
•简化代码审查：自动化工具可以发现许多共性问题，使代码审查者能更专注于业务逻辑和架构设计；
•减少线上故障损失：通过提前规避潜在风险，降低由于线上故障导致的各种损失。
研究内容
1.精确的TypeScript程序形式化建模：
•在保留TypeScript/ArkTS动态特性（如GC、事件、闭包等）的同时，构建足够精确的程序模型（如控制流图CFG、调用图CG、数据流图DFG）以支持深入分析；
•对框架等的运行时行为进行建模，以便分析框架之上应用代码的正确性；
•为TypeScript、ArkTS中的常见内存类缺陷（如内存泄漏、悬空指针、资源未释放等）建立有效的形式化分析模型。
2.高效的轻量级形式化分析算法：
•可扩展性：面对大型复杂应用(React/OpenHarmony等)，分析算法需要在合理的时间和资源消耗内完成；
•精度与时间的平衡：形式化验证往往通过完备建模牺牲误报(false positives)而保障无漏报(false negatives)。轻量级分析需要在保证一定精度、有限时间内和自动化能力的前提下，尽可能降低误报，避免给开发者带来过多干扰。
课题提供
•TypeScript和ArkTS的脱敏华为ICT、鸿蒙等项目程序和5+类缺陷案例；
年度目标
•（必选）提供基于TypeScript的形式化分析框架与缺陷检查器（能够覆盖5+类缺陷，如内存泄漏、undefined成员访问、越界访问、闭包泄漏、资源泄漏等），同时需要支持TypeScript框架编写的Web程序（如React框架编写Web应用）和ArkTS语言编写的鸿蒙应用；
•（必选）通过实际项目（如基于React的应用/OpenHarmony等真实应用）构建数据集，准确度、召回率>70%，百万行代码小于6h；
•（优选）支持其他TS框架如React Native,兼容 JavaScript融合部分代码的分析；
•（优选）支持联合Native语言的分析，如支持C++/C语言联合的形式化分析技术，以支持ArkTS与鸿蒙子系统交互、Web程序与浏览器交互等情形。
方向5:面向大规模代码的神经符号融合分析
课题背景
基于符号化的静态分析在不执行程序的情况下，以符号而非具体数值来分析该程序中所有可能的执行状态，从而检测程序潜在的问题、行为或性质。例如，路径敏感的数据依赖分析，通过沿着数据依赖关系追踪Source（例如a=nullptr）到Sink（空指针解引用处printf(*a)）再调用求解器判断相关路径条件是否可满足来检测空指针解引用缺陷。
但是传统静态分析工具面临三大技术与应用瓶颈：其一，在复杂数据与控制依赖场景下 (例如存在外部库函数，C++容器操作)，误报率居高不下；其二，对复杂程序语义（例如非标资源管理函数，程序输入/输出相关的高风险函数）未建模，分析存在显著漏报；其三，形式化技术的正确工程实现难度较大，常常因为工程问题导致分析器的漏报与误报。
通常来说，程序语义的完整表达呈现两个维度特征：一个维度体现于编程语言的结构化语义（数据依赖、控制流、类型系统等）；另一个维度则内嵌于自然语言载体（函数命名语义、变量命名惯例、文档注释等）。当前主流静态分析框架存在显著局限：仅聚焦结构化语义解析，忽视占代码信息量40%左右的自然语言元数据（据ICSE'22实证研究），导致程序意图推理的语义断层，限制分析的效果。
神经符号融合分析(Neuro-Symbolic Analysis)作为新一代静态分析范式，可以通过神经网络与符号化分析系统的协同分析实现突破：1）静态分析引擎借助形式化技术的可靠性，通过构建程序语义模型（如数据与控制依赖图）进行语义分析；2）神经网络组件突破传统静态方法局限，可实现基于源码的自然语言信息进行语义分析。
项目价值：
神经符号融合分析(Neuro-Symbolic Analysis)作为新一代静态程序分析范式，这种混合架构既保持符号系统可解释性优势，又具备深度学习对词法中自然语言信息的提取能力。因此，神经符号融合分析有望根本性解决传统静态分析的误报与漏报高的问题。
研究内容
本课题探索一种全新的神经符号融合分析框架，神经网络组件（以下简称为N）负责复杂API语义推断，例如非标内存管理函数识别，以及基于源码对Source到Sink进行路径敏感的分析，生成缺陷报告。静态分析引擎（以下简称为S）接收N推断的API信息，基于IR（代码中间表达式）进行路径敏感的分析，生成缺陷报告。已知S对程序语义的建模与工程实现，通过交叉对比两者的报告，可以提升S的准确度以及召回率：如果一个告警由N报出且S未建模相关语义，那么该告警很可能是S的漏报；如果一个告警由S报出但N未报出，那么该告警很可能是误报。现有学术界已经有很多静态分析的工作，但是如何利用神经网络组件对源码进行有效分析仍然未有充分探索，因此本项目主要针对N解决以下问题：
•利用AI技术进行复杂API语义智能推断（例如资源管理接口，程序输入/输出接口等高风险函数以及参数信息）；
•利用AI技术基于源码进行路径敏感的分析，生成缺陷报告；
•探索神经网络模型与静态分析技术融合的其他有前景的研究方向。
课题提供
•典型的产业应用静态分析工具问题场景；
•与业务场景中代码功能相似的开源代码；
•用于评估工具能力的benchmark。
年度目标
•（必要）利用AI技术对复杂API语义（例如资源管理接口，程序输入/输出接口等高风险函数）进行自动识别，分析准确度以及召回率达90%以上；
•（必要）利用AI技术对源码进行路径敏感的分析，支持两种以上缺陷的检查，缺陷报告结果与开源静态分析工具交叉对比（例如SVF，CSA），提升静态分析工具准确度以及召回率达30%以上；
•（优选）探索AI技术与静态分析技术融合的其它研究方向，可以解决漏报/误报/效率问题；
•（优选）支持多种语言（C/C++, TypeScript, Rust等）。
方向6:AI增强大规模 Trace 的预测分析技术
课题背景
随着并发/分布式软件复杂性的不断增加，如何高效发现系统中的潜在问题变得越来越重要。而基于程序执行事件轨迹（即trace，事件包括线程创建、锁操作、共享内存访问、同步点等）的预测分析技术被证明是一种行之有效的方法，它可以根据某次动态执行获得的轨迹判断程序是否存在死锁、资源竞争等并发问题。需要强调的是它的问题发现能力不局限在当前轨迹，预测分析算法会根据事件之间的偏序关系推断出当前轨迹的合法变种是否存在问题，从而极大提高问题发现效率。相较于其它并发问题发现技术，预测分析对编程语言、运行环境没有过多要求，且具有理论上的正确性保证（无误报），具有很好的通用性。
然而，现有先进预测分析技术距离实际应用还有不小差距：1.预测分析算法高度依赖轨迹质量，如果轨迹不全（如实际场景中常见的关键事件没有录到或事件之间的结对关系缺失）算法将丧失理论上的正确性保证，导致误报率飙升；2.传统预测分析方法无法处理过长的轨迹或3.含有过多线程的轨迹，如面对10万级事件或数百个线程规模的分析，预测分析技术面临时间复杂度高、内存爆炸的问题，即便最先进的算法也难以完成。
因此，本项目旨在通过引入前沿的AI辅助方法，开发一种高效、可扩展的预测分析技术框架，提高针对大规模轨迹的预测准确度，降低计算成本。从而为大规模并发/分布式系统的可靠性提供更高的保障。
项目价值：
本课题有较高的学术价值，且对于提升并发/分布式系统的可靠性有重要意义。并发问题的高效发现一直是学术界和业界的难点，预测分析技术因其原理上的通用性和理论上对正确性的保证近年来备受关注。然而当前多数研究工作聚焦在较理想化的场景，对于现实中轨迹不全、轨迹规模过大的问题没有很好的解决方案。同时目前已经有一些前沿研究尝试通过生成式模型解决轨迹重建等相关的问题并展现出较高的可行性，如何借助AI的力量解决预测分析技术中的关键难题既有较高的学术价值，同时对于提升并发/分布式系统的可靠性有重要意义。
研究内容
大规模轨迹预处理与优化：
•轨迹补全，通过AI分析不完整的轨迹日志（可结合程序源代码），对轨迹进行重建和补全，提升trace质量，减少后续分析的误报；
•轨迹剪枝，通过AI和/或基于规则的方法分析轨迹中的事件类型（可结合程序源代码），过滤与程序并发行为无关的事件，减少trace的大小，提升后续分析效率；
•模块化拆分，并发/分布式系统中并不是所有部分都有相互影响，例如一个程序中线程a只和b有交互行为，线程c只和d有交互行为，此时可以把包含a, b, c, d所有事件的巨大轨迹拆分为分别包含a事件∪b事件和c事件∪d事件的两个较小轨迹独立分析，理论上此举可极大降低分析的时间和空间开销。此课题拟通过AI和/或基于规则的方法分析轨迹中事件之间的关系（可结合程序源代码），将一个大规模轨迹拆分为若干规模较小的模块（每个模块可以认为是仅包含部分事件及其对应的后续分析所需要的偏序关系的闭包），以降低分析复杂度。
AI预测分析算法：
•见证生成，见证（witness）指预测分析算法报告的存在问题的轨迹，传统由确定性算法通过对轨迹中事件之间关系的计算得出，但在线程较多等情况下，现有算法往往因其技术原理的限制无法完成分析。此项研究拟构建基于AI Agent的启发式方法，高效发现现有轨迹中的问题或根据现有轨迹生成问题轨迹见证，并结合基于规则的判定方法减少误报。
课题提供
•本项目提供开源项目作为测试集。
年度目标
•（必要）提供轨迹预处理技术，包含：轨迹补全功能，对于缺失事件补全操作的正确率达到60%+；轨迹剪枝功能，对于并发无关事件正确滤过率达到60%+；模块化拆分功能，在至少3个轨迹上展示拆分效果（可将每条原始轨迹拆分为至少2条新轨迹）并展示拆分后的分析结果等价于拆分前。
•（必要）提供witness生成技术，可接受10万个事件规模的轨迹，支持包括死锁和资源竞争在内至少2类问题的报告，witness生成的精确率（precision）达到80%+。
申请截止日期：2025年8月31日24:00
如何申报：
来源：CCFvoice
