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

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
2025,36(8):3429−3430 [doi: 10.13328/j.cnki.jos.007355] [CSTR: 32375.14.jos.007355] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

*
形式化方法与应用专题前言

陈明帅 1 , 田 聪 2 , 熊英飞 3

1
(浙江大学 计算机科学与技术学院, 浙江 杭州 310027)
2
(西安电子科技大学 计算机科学与技术学院, 陕西 西安 710126)
3
(北京大学 计算机学院, 北京 100871)
通信作者: 陈明帅, E-mail: m.chen@zju.edu.cn; 田聪, E-mail: ctian@mail.xidian.edu.cn;
熊英飞, E-mail: xiongyf@pku.edu.cn

中文引用格式: 陈明帅, 田聪, 熊英飞. 形式化方法与应用专题前言. 软件学报, 2025, 36(8): 3429–3430. http://www.jos.org.cn/1000-
9825/7355.htm

形式化方法基于严格的数学化和机械化方法来规约、设计、构建、验证、演进计算系统, 是改善和确保计算
系统质量的重要方法, 其模型、技术和工具已延伸成为计算思维的重要载体. 本专题聚焦形式化方法理论前沿, 围
绕形式化方法基础理论、技术、支撑工具及领域应用, 重点关注形式化方法与理论计算机科学、软件工程、基础
软件 (操作系统、编译器等)、嵌入式系统、人机物融合系统、概率/量子系统、网络与信息安全、可信人工智能
(智能制造、智能交通、智能控制、可信机器学习) 等领域的交叉结合, 旨在于我国标志性学术刊物上反映形式化
方法领域的最新研究成果, 深入拓展形式化方法与相关领域的交叉, 促进形式化方法、技术和工具在国内的应用
和发展.
本专题采取公开征文的方式, 共收到投稿 18 篇, 先后邀请了 30 余位相关领域专家参与审稿工作, 每篇投稿邀
请了 2–3 位专家进行评审. 稿件经初审、复审、ChinaSoft 2024 中国软件大会“形式化方法与应用专题论坛”汇报
和终审 4 个阶段, 历时 6 个月, 最终有 12 篇论文入选本专题.
论文《Fast-USYN: 从酉矩阵到高质量量子电路的快速合成》提出了一种根据酉矩阵合成量子电路的快速合
成方法 Fast-USYN, 相较于当前最优的合成方法实现了门数量减少、速度提升的显著性能优化.
论文《神经网络的增量验证》针对神经网络结构与参数修改后的安全性质验证需求, 提出了一种基于
Reluplex 框架的增量可满足性模理论算法 DeepInc, 实现了相较于 Marabou 和 α, β-CROWN 的显著加速.
论文《单球驱动平衡机器人运动学和动力学形式化验证》基于定理证明器 HOL Light 及其数学、物理学相
关的定理证明库, 实现了在高阶逻辑框架下对单球驱动平衡机器人运动学与动力学模型的构建、推导与证明.
论文《基于记忆策略的元解释学习》针对元解释学习中的冗余证明问题, 提出了一种基于 Prolog 数据库机
制的剪枝策略, 证明了其正确性, 在理论上计算了程序空间的缩减比例, 并实证了其对现有系统学习时间的优化.
论文《GhostFunc: 一种针对 Rust 操作系统内核的验证方法》面向基于 Rust 构建的微内核中 unsafe 代码段
的验证需求, 提出了 GhostFunc 的 safe 和 unsafe 代码段组合验证方法, 针对任务管理与调度模块在交互式定理证
明器 Coq 中完成了正确性验证.
论文《面向自动驾驶系统的场景建模及边缘关键场景生成》基于自动驾驶领域本体建模场景, 结合形式化量
化评估与重要性采样, 提出并实现了一种基于 SML4ADS2.0 的自动驾驶场景建模及边缘关键场景生成方法.
论文《动态顺序统计树类结构的函数式建模及其自动化验证》针对动态顺序统计树结构这类数据结构, 设计
了函数式建模方法和自动化验证方法, 可对模型中的数据结构实例自动生成正确性验证.
论文《基于下推自动机的同步数据流语言可信编译》提出了同步数据流语言可信编译方法, 可将 Lustra 语言

* 收稿时间: 2024-12-11; jos 在线出版时间: 2024-12-11