近日，由中国计算机学会（CCF）主办的2023年中国软件大会（ChinaSoft）在上海召开，大会公布了CCF专业委员会2023年度“博士学位论文激励计划”入选名单。中国科学院软件研究所冯胜华博士（指导教师：詹乃军研究员）和燕季薇博士（指导教师：严俊研究员）的论文分别入选CCF形式化方法专业委员会和软件工程专业委员会2023年度“博士学位论文激励计划”。 

　　冯胜华，2023届毕业生，现在中关村实验室从事科研工作。其博士学位论文《概率与随机系统的形式验证》围绕复杂信息物理融合系统中的随机特性，关注概率与随机系统的形式验证问题。概率与随机系统是一类刻画系统随机性的形式模型，在多个领域中有着广泛的应用。论文发展了概率程序和随机动态系统关键性质的验证能力，在随机系统的形式验证理论上做出基础性贡献。针对概率程序定量性质的验证，论文首次解决了发散概率程序的不动点下界验证问题，突破了已有方法无法验证发散概率程序的局限性；针对随机动态系统的安全性验证，论文提出了基于归约的验证方法，大幅提升了系统安全概率估计的准确度；此外，论文进一步将安全性验证推广至容忍安全性验证并给出验证方法，为系统的安全性提供了更加精细的刻画。 

　　燕季薇，2023届毕业生，现为软件所软件工程技术研究开发中心助理研究员。其博士学位论文《基于框架与应用协同分析的安卓应用质量保障技术研究》关注基于复杂编程框架的移动应用程序质量保障自动化技术，采用字节码静态分析技术提取框架代码信息，基于框架信息开展上层应用分析测试，有效解决了复杂框架特性导致的上层应用缺陷难以被触发、重现和定位等问题。在框架级信息提取方面，构造了包含框架级组件通讯ICC消息测试预言的公开数据集，并设计了先进的框架级信息解析方法，相比国际主流同类工具，在精度和效率方面均有显著提升。在基于框架级信息的应用质量保障方面，提出了一套面向上层应用的测试用例生成方法，触发了大量隐藏崩溃；提出了高效的测试序列约减策略，快速找到崩溃触发子序列；提出了面向框架级崩溃错误定位方法的新思路，有效提高了定位精度并减小了候选集规模。 

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