Page 7 - 《软件学报》2025年第8期

3430 软件学报 2025 年第 36 卷第 8 期

程序转换为 C 语言程序, 并使用 Isabelle 对翻译转换过程进行严格的正确性证明.
论文《操作系统内核权能访问控制的形式验证》以并发精化程序逻辑 CSL-R 为基础, 通过证明权能 API 函
数和其抽象规范之间的精化关系, 来验证航天嵌入式领域某微内核操作系统权能访问控制的功能正确性.
论文《基于混成自动机路径过滤与动态选择的 CPS 系统反例生成》针对 CPS 系统中生成反例的路径爆炸问
题, 提出了路径过滤与动态选择两种技术, 可提高 CPS 系统反例生成的效率和性能.
论文《面向 Rust 语言的形式化验证方法研究综述》综述了 Rust 语言的形式化验证工作, 通过语义模型、自
动化验证方法及实例分析, 探讨了提升 Rust 安全性的途径与挑战, 并展望了未来研究方向.
论文《因果时空语义驱动的深度强化学习抽象建模方法》针对智能信息物理融合系统中深度强化学习决策
效率低下和泛化性不足的问题, 提出基于因果时空语义的深度强化学习抽象建模方法, 通过实验验证了该方法在
抽象表达能力、准确性及语义等价性方面的效果.
本专题主要面向形式化方法的研究人员和采用形式化方法开展软件设计开发、软件分析验证、工业应用的
工程技术研发人员, 反映了我国学者在形式化方法与应用领域最新的研究进展. 感谢《软件学报》编委会和 CCF
形式化方法专委会对专题工作的指导和帮助, 感谢专题全体评审专家及时、耐心、细致的评审工作, 感谢踊跃投
稿的所有作者. 希望本专题能够对形式化方法与应用相关领域的研究工作有所促进.

陈明帅(1990－), 男, 博士, 浙江大学研究员, 博士生导师, CCF 高级会员, 形式化方法专委执行委员, 杭州市钱江特聘专
家, 国家优秀青年科学基金 (海外) 获得者. 主要研究领域为形式验证, 程序理论, 概率/量子系统, 信息物理融合系统等.
与合作者一起, 提出新型安全攸关系统形式验证理论, 解决了概率程序不动点估计、微分系统可达性判定、时滞系统
高效控制生成等若干软件理论难题, 研究成果应用于我国探月二期工程“嫦娥”三号等重大工程, 在 Information and
Computation、OOPSLA、CAV、FM、ASPLOS 等领域旗舰期刊/会议上发表学术论文 30 余篇, 曾获中国科学院院长
特别奖、ATVA 杰出论文奖、FMAC 最佳论文奖.

田聪(1981－), 女, 博士, 西安电子科技大学二级教授, 博士生导师, CCF 杰出会员, 科学研究院院长, 陕西省安全攸关智
能软件重点科技创新团队负责人. 担任中国计算机学会形式化方法专委会副主任、中国自动化学会网络信息服务专委
会副主任、全国信息技术标准化技术委员会软件与系统工程分技术委员会委员; 《软件学报》、IEEE Trans. on
Reliability、Journal of Combinatorial Optimization、《西安电子科技大学学报》等期刊编委. 长期从事可信软件、形式
化验证理论与方法研究.

熊英飞(1982－), 男, 博士, 北京大学长聘副教授, CCF 专业会员, 软件研究所副所长. 主要研究领域为程序合成、修复、
分析和验证. 工作帮助产生了一系列不同规模的效果同期最优代码生成神经网络模型, 如 DeepSeek-Coder 模型; 大幅提

升了缺陷修复的正确率、修复数量和修复效率; 提出了最广泛使用的两大双向变换模型之一——基于差别的双向变换;
成功自动求解大量算法问题, 包括世界顶级算法竞赛中的问题. 在 IEEE TSE 担任编委, PLDI、ICSE、FSE、OOPSLA、
ASE、ISSTA 等会议定期担任 PC, 5 次在 ICSE 和 FSE 会议上获得杰出审稿人奖. 获得国家技术发明一等奖 (排名 6)、
电子学会自然科学一等奖 (排名 1)、CCF-IEEE CS 青年科学家奖、MODELS 十年最有影响力论文奖, 5 次获得 ACM SIGSOFT/IEEE
TCSE 杰出论文奖, 是 IFIP WG 2.4 唯一来自中国的成员.