评审结果公示 | 2025年度CCF-华为胡杨林基金-形式化专项

近期，2025年度CCF-华为胡杨林基金-形式化专项完成评审，共10位学者获得本年度基金资助，现予以公示。

2025年度CCF-华为胡杨林基金-形式化专项于2025年7月5日发布申报课题方向指南，并同步开启申报。

本年度共6个产业课题方向：

1、基于大模型的可形式化证明代码生成 

2、面向形式化验证的RUST通用借用演算中间语言技术

3、基于TLA⁺模型的设计与代码功能一致性检查技术

4、面向TypeScript语言的轻量级形式化分析

5、面向大规模代码的神经符号融合分析

6、AI增强大规模Trace的预测分析技术

产业课题主要针对产业典型问题，持续提升形式化技术的能力上界、降低业界应用相关技术的门槛和成本，创造产业价值，形成本基金的正循环。

开放课题不限定具体研究内容，主要资助具有前瞻性、前沿性、能为产业全面升级储备能力，实现关键基础技术底座自主、领先的相关课题。

至申报截止时间：2025年8月31日24:00，共收到项目申请书39份，其中产业课题申请14份，开放课题申请25份。

9月15日~9月22日，CCF形式化专委会和华为各三位专家组成的技术委员会对项目申请进行了预审评分。

产业课题围绕课题相关性、研究背景匹配度、技术先进性及合理性、项目交付风险、交付件、可落地性六个维度分别打分；

开放课题围绕形式化技术/产业课题相关性、研究背景匹配度、技术先进性及合理性、研究计划、交付件、应用价值六个维度分别打分；

9月23日晚召开了技术委员会线上会议，对项目申请进行正式评审，采取同单位专家回避原则，在专家充分发表意见的基础上，以全员表决的方式确定最终资助项目。本次评审过程的所有信息均备案可查。

经技术委员会评审，最终确定本年度资助产业课题方向项目5个，开放课题项目5个。

按计划，本年度资助项目于2025年12月开题，2026年6月中期审视，2026年12月进行答辩结题。

10个资助项目信息如下：

中国科学院软件研究所特别研究助理。2019年获北京大学学士学位，2025年获中国科学院软件研究所博士学位，博士期间师从蔡彦研究员。主要研究方向为软件分析与测试，重点聚焦于并发软件的缺陷检测理论与方法，研究成果发表于ICSE、ESEC/FSE等软件工程国际顶级会议/期刊，多项研究成果已在产业实际场景中落地应用，参与国家重点研发计划、中国科学院先导等项目。

现任南京大学软件学院助理研究员，于南京大学获软件工程博士学位，并曾在博士期间赴瑞士ETH Zurich访学。主要研究方向为软件测试与分析方法，重点聚焦于移动应用，尤其是安卓应用的可靠性与安全性保障。除此之外，亦长期关注程序逆向领域，包括Java程序逆编译、代码混淆与反混淆等方向。在国际软件工程与程序语言领域的顶级期刊与会议TOSEM、ISSTA、FSE、ASE、ICSE、OOPSLA等发表论文十余篇，主持一项国家自然科学青年基金项目及多项企业创新项目。

上海交通大学John Hopcroft计算机科学中心副教授，此前于美国耶鲁大学计算机系担任博士后研究员，博士毕业于美国明尼苏达大学双城分校计算机系。长期从事形式化方法方面研究，内容涵盖软件形式化验证、程序设计语言理论（包括程序语义、逻辑框架等）、以及它们在关键性系统软件（如编译器和操作系统）中的应用，代表性成果发表于形式化验证和程序设计语言方向的国际顶会（POPL、PLDI、OOPSLA、CAV等）。定理证明工具Abella（http://abella-prover.org）的核心设计和开发人员。

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

南京大学教授，主要研究领域为并发与分布式系统、软件形式化验证。在EuroSys、ATC、PODC、IEEE TC、IEEE TPDS等国际会议与期刊上发表学术论文多篇。主持国家自然科学基金、CCF-华为胡杨林基金、阿里云创新研究计划等多项科研项目。2014年获南京大学登峰人才支持计划资助，协助指导的博士论文获得2016、2017年度中国计算机学会优秀博士论文奖，2022年获SRDS会议最佳论文奖。建设了南京大学“百层次”优质课程《算法设计与分析》，2018年入选首届高校计算机专业优秀教师奖励计划，2024年获评江苏省一流本科课程。

中国科学院软件研究所特别研究助理，CCF形式化方法专委会通讯委员。主要从事形式验证、程序理论、信息物理融合系统、混成系统等方向的研究，研究成果广泛发表于CAV、FM、OOPSLA、IEEE TAC等形式化领域高水平国际会议期刊。主持国家自然科学青年基金（C类）项目，作为骨干成员参与多个国家自然科学基金重点、重大项目，博士论文入选CCF形式化专委会博士学位论文激励计划。

西安电子科技大学计算机科学与技术学院讲师，CCF形式化方法专委会通讯委员。博士就读于航天五院502所，主要研究方向为嵌入式系统和形式化验证。近年作为骨干成员参与国自然重大、重点项目的研究工作，在ASE、ACM MM、JSTAR、Information Fusion、软件学报等会议与期刊上发表论文十余篇，主持面向国家重大航天工程的产学研合作课题六项，参与设计并验证了我国新一代空间操作系统SpaceOS II，目前已稳定在轨应用于嫦娥、天宫、天问等型号任务。

中科工业人工智能研究院特别研究助理。2025年于中国科学院软件研究所获得博士学位。主要研究方向为可满足性模理论(SMT)的求解与应用。在CAV、FM、ICSE、ToCL、CP、IJCAI等重要国际期刊/会议发表学术论文10余篇，多次获得国际SMT比赛冠军（包括国内首次在该赛事夺冠）。曾获得中国科学院院长优秀奖、入选CCF形式化专委博士论文激励计划。

华东师范大学软件工程学院青年研究员、博士生导师。2021年博士毕业于上海交通大学，随后在英国牛津大学和新加坡南洋理工大学从事博士后研究工作。研究方向聚焦于形式化方法，涵盖可信人工智能、程序验证以及AI+FM的交叉研究，致力于通过逻辑推理与数学证明，实现智能系统的自动化可信保障。近年来，相关成果发表于POPL、PLDI、OOPSLA、CAV、NeurIPS、AAAI等国际顶级会议。担任多个国际顶级会议审稿人（NeurIPS、ICML、ICLR、AAAI、AISTATS）以及工件评审委员（POPL、PLDI、CAV）。

现任南京大学计算机学院副教授、博士生导师，2024年入选国家自然科学基金优秀青年科学基金项目（海外）。自2024年初起在斯坦福大学担任访问教授（Sponsor：斯坦福大学计算机系前主任Alex Aiken教授）。其主要研究方向涵盖编程语言、程序分析和机器学习，相关成果发表在PLDI、OOPSLA、NeurIPS、ICLR和IJCAI等国际顶级会议，其中OOPSLA 2020论文获杰出论文奖，多篇论文在机器学习顶会评为oral、spotlight。曾任Visa研究院首席研究科学家，微软研究院Redmond研究科学家。于加州大学戴维斯分校获得计算机科学博士学位，在读期间于2015年和2018年两度荣获计算机科学系杰出博士生荣誉提名。此外，还具有西门子美国、西门子中国研究院及Meta（原Facebook）公司的研发工作经历。