本年度共设6个产业课题方向：
1) 可追溯的中间代码元数据生成；
2) 面向Rust+C大规模代码的内存与并发缺陷分析技术；
3) 基于抽象解释的RUST高效内存安全验证工具；
4) 面向形式化验证的可靠二进制提升技术；
5) 基于自动推理的ACSL规约生成；
6) 可证明低代价大模型修复方法。
开放课题不限定具体研究内容，主要资助具有前瞻性、前沿性、能为产业全面升级储备能力的课题。
至截止时间（2024年9月30日24:00），共收到项目申请书36份，其中产业课题10份，开放课题26份。
评审由CCF形式化方法专委会和华为各自派驻3位专家组成的评审委员会组织推进，评审分为通讯评审和会议评审两个阶段，采取了同单位专家回避原则。
在第一阶段中，评审委员会从10月15日到10月21日对项目申请进行了通讯评审。对于产业课题，评审专家按照课题相关性、研究背景匹配度、技术先进性及合理性、项目交付风险、研究计划、交付件、可落地性等七个纬度进行了评分，每个项目申请最终分数为这七项评分之和。对于开放课题，评审专家按照形式化技术/产业课题相关性、研究背景匹配度、技术先进性及合理性、研究计划、交付件、应用价值等六个纬度进行了评分，每个项目申请最终分数为这六项评分之和。每个项目申请通讯评审最终得分为所有评审专家分数的平均值（同单位专家除外）。
在第二阶段中，10月22日晚评审委员会召开线上会议，对CCF-胡杨林基金形式化方法专项项目申请进行了会议评审。会议评审由华为形式化验证科学家、费马实验室主任秦胜潮主持，采取同单位专家回避原则，在专家充分发表意见的基础上，以全员表决的方式确定最终资助项目。本次评审过程的所有信息均备案可查。
最终，经过评审委员会两个阶段的评审，确定了2024年度资助产业课题项目4项、开放课题项目5项。按计划，本年度资助项目于2025年1月开题，2025年6月中期审视，2025年12月进行答辩结题。
9个资助项目信息如下（排名不分先后）：
姓名 | 单位 | 课题类型 | 项目名称 |
时清凯 | 南京大学 | 产业课题 | 面向跨语言（Rust/C）代码的内存与并发缺陷分析技术研究 |
符鸿飞 | 上海交通大学 | 产业课题 | 基于约束求解方法的ACSL规约生成 |
王竟亦 | 浙江大学 | 产业课题 | 大模型缺陷根因溯源及定向可证明修复方法研究 |
周明洋 | 深圳大学 | 产业课题 | 基于贝叶斯估计和数据分布扰动的大模型修复方法 |
罗川 | 北京航空航天大学 | 开放课题 | 布尔可满足性采样技术研究 |
张羽丰 | 湖南大学 | 开放课题 | 基于符号执行、采样及模糊测试的混合测试方法 |
袁胜浩 | 浙江大学 | 开放课题 | eBPF Just-In-Time编译器端到端形式化验证方法 |
潘颖慧 | 深圳大学 | 开放课题 | 基于表示工程的大语言模型输出可读性技术研究 |
曹永知 | 北京大学 | 开放课题 | 线性时序逻辑合成问题的关键技术研究及其实现 |
时清凯
南京大学计算机学院副教授，博士生导师，紫金学者，国家级高层次青年人才，2020 年于香港科技大学获得博士学位，曾任源伞科技联合创始人、蚂蚁集团技术专家、美国普渡大学博士后研究员。目前主要从事编译技术及基于编译的软件安全技术研究，其研究成果广泛发表于程序语言（如 PLDI，OOPSLA）、软件工程（如 ICSE，ESEC/FSE）、网络安全（如SP，CCS）等 CCF A 类会议或期刊，曾获 ACM SIGSOFT 杰出论文奖、ACM SIGPLAN杰出论文奖、Google 论文奖、Hong Kong PhD Fellowship。其研究成果广泛应用于诸如蚂蚁、华为等高新技术企业，已帮助企业识别数百个高危软件安全漏洞。
符鸿飞
上海交通大学副教授，博士毕业于德国亚琛工业大学。长期从事形式验证前沿理论的研究，成果多发表在POPL、PLDI、CAV、OOPSLA、TOPLAS等程序语言与形式化方法著名国际学术会议与期刊上。提出非确定性概率程序终止性验证的鞅理论框架，并通过线性以及多项式约束求解方法给出了概率程序终止性的检验算法。提出概率程序灵敏性验证的鞅理论框架。通过显著推广经典的鞅停时定理解决概率程序资源消耗的定量分析问题。针对概率程序的断言分析建立不动点理论刻画并通过设计凸优化算法给出了第一个求解指数不动点的完备算法。通过鞅理论的约束求解给出了概率递归关系尾概率分析的新方法，其显著改进Karp经典方法所导出的渐进尾概率上界。提出基于截断的概率程序贝叶斯推理静态分析框架。在循环不变式自动生成的约束求解方法方面有诸多建树。发表概率程序终止性验证专著章节，由国际著名出版社剑桥大学出版社出版。
王竟亦
浙江大学研究员、博导。博士毕业于新加坡科技设计大学，新加坡国立大学博士后。主要研究兴趣是形式化方法与安全、智能软件工程。在多个相关领域国际顶级会议和期刊如S&P、CCS、ICSE、TSE、FM、TACAS等发表论文40余篇，获得了两次ACM SIGSOFT杰出论文奖（ICSE 2018和ICSE 2020)，并入选ACM SIGSOFT Research Highlights。担任ACM CCS、ICSE、ISSTA等程序委员会委员及TSE、TOSEM、TDSC等审稿人。主持了国家重点研发子课题、浙江省 “尖兵”课题、NSFC青年基金、CCF-华为胡杨林基金、蚂蚁金服/华为产业课题等。获2024年中国指挥与控制学会科技进步一等奖。
周明洋
深圳大学计算机与软件学院副教授，硕士生导师。2016年毕业于中国科学技术大学获得工学博士学位。主要研究方向为复杂网络信息传播、图数据挖掘、分布式联邦学习。主持国家自然科学基金面上项目、青年项目及省、市项目。相关成果发表在会议NeurIPS,WWW,KDD,IJCAI,ENMLP和期刊等四十余篇。作为主要作者完成两本编著《大数据计算理论基础》（2017）、《大数据计算方法基础》（2023）。担任多个高水平期刊审稿人。
罗川
北京航空航天大学软件学院副教授，博士研究生导师，现任北京航空航天大学软件学院关键基础软件所副所长。已入选中国科协青年人才托举工程、CCF青年人才发展计划。迄今总计发表CCF-A类论文40余篇，谷歌学术引用超过1900次。担任多个CCF-A类国际顶级会议的（资深）程序委员会成员。作为负责人主持多项科研项目，包括国家重点研发计划课题、国家自然科学基金项目等。在国际知名约束求解竞赛（国际SAT求解竞赛、国际MaxSAT评测竞赛）中共获得了17次冠军，包括获得亚洲首冠。所提出的约束求解技术被国际知名学者（包括诺贝尔奖得主等）实际使用，帮助取得了巨大的经济效益；同时，研究成果被顶尖科技企业（包括国家电网、华为、微软等）应用落地，有效提升了关键系统软件的性能和可靠性。
张羽丰
湖南大学信息科学与工程学院副教授，博士生导师，CCF形式化方法专委会委员。本硕博毕业于国防科技大学计算机学院，毕业后任战略支援部队第56研究所助理研究员，2020年加入湖南大学信息科学与工程学院。研究方向为高可信软件、程序分析与测试、人工智能。主持国家自然科学基金青年/面上项目、工信部某重大专项子课题、CCF-华为胡杨林基金等多项项目，参与多项973、863、核高基、科技部重点研发、国防预研等项目。在ICSE、ASE、FSE、ISSTA、ISSRE、IEEE-TSC、NeurIPS、TKDE等顶级国际会议及期刊上发表论文十余篇。
袁胜浩
浙江大学区块链与数据安全全国重点实验室研究员。在法国国家信息与自动化研究所INRIA攻读理论计算机博士学位（2020-2023）。主要研究方向为形式化方法、编译器、虚拟机、区块链、操作系统安全等。致力于使用形式化验证技术，尤其是基于定理证明工具Coq和Isabelle/HOL验证包括Linux和RIOT-OS在内的多种eBPF虚拟机、编译器、解释器的安全性。在理论计算机国际顶级会议CAV22和CAV24（CCF-A类）中以第一作者+通信作者身份发表论文。
潘颖慧
深圳大学大数据系统计算技术国家工程实验室副教授。CCF协同计算专委会执行委员、中国系统工程学会信息系统工程专业委员会理事。主要从事多智能体系统、概率图模型、不确定性人工智能领域的研究工作。国家公派留学在丹麦奥尔堡大学联合培养博士，英国提赛德大学访问学者，对多智能体系统领域有深厚的理论基础，深入研究了无人驾驶飞机追踪、服务创新、台风预警等不确定环境下的多智能体决策应用问题。近年来主持国家自然基金面上项目、国家自然基金青年项目、国家重点研发计划子课题、广东省自然基金面上项目等，有丰富的项目研究经验。在国内外权威期刊和国际顶级会议上发表相关论文多篇。此外，还担任十余个包括AAAI、IJCAI、AAMAS等国际顶级会议的程序委员会委员和TKDE、TSMC、INS、KBS、计算机学报、软件学报等期刊的审稿人。
曹永知
北京大学计算机学院教授、博士生导师，教育部网络空间安全专业教指委委员，IEEE高级会员，中国网络空间安全人才教育联盟副理事长，CAAI离散智能计算专委副主任，CCF形式化方法专委和理论计算机科学专委执行委员。近年来主要从事形式化方法、数据隐私性与安全性、社会计算等方面的研究，在AAAI，AIJ，IEEE TAC，IEEE TC，IandC，IJCAI，JCSS，TCS，《中国科学》等国内外知名期刊或会议上发表学术论文100余篇。作为项目负责人主持国家自然科学基金5项，作为课题负责人主持科技部重点研发计划重点专项1项，作为第一完成人获教育部自然科学二等奖1项。
编辑、审核：大可
版权声明：本文由“TOP大学来了”综合自“中国计算机学会”，文章转摘只为学术传播，如涉及侵权问题，请联系我们，我们将及时修改或删除。
