2025年中国计算机学会（CCF）中国软件大会于11月28日至30日召开。期间，CCF系统软件专业委员会和形式化方法专业委员会公布了2025年度博士学位论文激励计划评选结果，中国科学院软件研究所马旭桐博士（指导教师：张健研究员）和李博涵博士（指导教师：蔡少伟研究员）的论文分别入选。

马旭桐，2024届博士毕业生，现为法国国家信息与自动化研究所博士后。其博士学位论文《C/C++ 程序新型内存操作缺陷的高效静态检测》聚焦于C/C++程序的静态分析，以发现系统软件中常用的内存管理机制的使用错误。论文针对系统软件开发者常用的智能指针和引用计数机制，提出了对新型内存操作及其背后机制的建模方法，并对相关误用进行了检测。同时，论文也对建模导致的额外时间开销，以及分析方法导致的相似报告等问题提出了基于分析并行化和冗余报告消除的优化方案。开发的多个工具在数据库管理系统、AI基础软件库中发现了数百个真实的缺陷，并得到开发者的修复。相关工具也在知名商业公司和开发平台中进行了试用，受到了开发者和使用者的广泛好评。

李博涵，2025届博士毕业生，现在中科工业人工智能研究院担任助理研究员。其博士论文《算术理论SMT问题的局部搜索算法与应用》围绕算术理论可满足性模理论（SMT）问题展开研究。SMT求解器作为软件可靠性保障的计算引擎，在软件验证和测试等领域有重要应用。论文提出了首个针对整数算术理论SMT问题的局部搜索算法LocalSMT，弥补了该领域的研究空白。该算法采用新颖的双模式搜索框架，并设计了临界移动运算符与细粒度评分函数。论文还进一步将局部搜索技术拓展至实数算术理论，提出了基于区间的运算符和相应的松弛方法。LocalSMT对可满足算术理论实例的性能达到了国际领先，尤其对非线性算术理论实例的求解性能大幅超过前沿求解器。基于LocalSMT算法的求解器在国际 SMT 比赛获得多次“最大领先奖”和“最大贡献奖”，包括我国在SMT比赛的首个冠军。论文将LocalSMT应用于终端设备的页面自动布局，支持页面布局的“一次开发，多端部署”，并实现毫秒级响应。该项目获得华为“鸿蒙创新大赛” 冠军，并被华为确定为鸿蒙系统的新特性。

CCF专业委员会“博士学位论文激励计划”旨在进一步推动软件领域高水平创新人才培养工作。评选采用推荐-评审制，由单位推荐或CCF会员联名推荐候选博士学位论文、各专业委员会组建的该计划评审委员会组织评审，评选过程具体包括推荐、资格审查、初评、终评四个阶段。各专业委员会每年评选出不超过3篇在相关领域做出杰出创新研究工作的博士学位论文，对论文完成人给予表彰和奖励。