形式化方法以严格的数学化和机械化方法为基础来规约、设计、构建、验证、演进计算系统，是改善和确保计算系统质量的重要方法，其模型、技术和工具已成为安全攸关系统质量保障不可或缺的重要载体。形式化方法已经成功应用于各种硬件（如芯片）的设计，各大硬件制造商（如IBM、AMD等）都有一支强大的形式化方法团队，为保障系统的可靠性提供技术支持。近年来，随着形式验证技术和工具的发展，特别是在程序验证中的成功应用，形式化方法在处理软件开发复杂性和提高软件可靠性方面已显示出无可取代的潜力。著名的研究机构都投入了大量人力和物力从事这方面的研究。例如，美国宇航局（NASA）拥有一支庞大的形式化方法研究团队，在保障美国航天器控制软件正确性方面发挥了巨大作用；又如，中国航天科技集团公司五院自主研发的航天操作系统SpaceOS、华为自主研发的鸿蒙操作系统HarmonyOS等，均使用了形式化方法，从根本上确保系统设计的无差错和高可靠。在新兴领域，如区块链、可信人工智能等领域，形式化方法也逐步应用适配，提升系统的整体安全可控。

本专刊围绕形式化方法基础理论、技术、支撑工具及领域应用，重点关注形式化方法与理论计算机科学、软件工程、基础软件（操作系统、编译器等）、嵌入式系统、人机物融合系统、概率/量子系统、网络与信息安全、可信人工智能（智能制造、智能交通、智能控制、可信机器学习）等领域的交叉结合。拟收录相关方向的综述或突破性的关键理论、关键技术以及得到工业应用的工具等相关论文。

经过第一轮评审的论文作者需要参加ChinaSoft 2024会议（https://chinasoft.ccf.org.cn/）并到会报告，之后特约编辑和编辑部根据复审情况和会议报告情况决定文章的最终结果，专刊将在2025年第8期出版。读者群体包括形式化方法、软件工程、嵌入式系统、可信人工智能等多个领域的研究人员和工程人员。

专刊题目：形式化方法与应用
特约编辑：陈明帅（浙江大学）田聪（西安电子科技大学）熊英飞（北京大学）
出版时间：2025年第8期

一、征文范围
包括但不限于以下主题：
1. 形式化方法理论、方法、技术与工具：
（1）模型检验
（2）定理证明
（3）静态分析与运行时验证
（4）约束求解与判定过程
（5）规约、构造与类型系统
（6）SMT与SAT求解
（7）模型驱动开发
（8）程序合成
（9）形式化方法中的机器学习与概率推理
（10）形式化方法与仿真、测试的组合
（11）形式化方法支撑工具
2. 面向特定应用的形式化方法：
（1）可信人工智能
（2）区块链
（3）量子计算
（4）智能制造
（5）人机物融合系统
（6）特定软件系统的智能合成与验证
（7）芯片设计与软硬件协同
（8）信息安全与隐私

二、投稿要求
1. 投稿方式：采用“软件学报在线投稿系统”(http://www.jos.org.cn)投稿。投稿时请选择投稿类型为“专刊投稿”，并在备注栏中注明“形式化方法与应用”字样。
2. 稿件格式：参照《软件学报》论文格式(网站上提供了论文模版，可下载)。
3. 投稿文章未在正式出版物上发表过，也不在其他刊物或会议的审稿过程中，不存在一稿多投现象；保证投稿文章的合法性(无抄袭、剽窃、侵权等不良行为)。
4. 其他事项请参阅投稿指南http://www.jos.org.cn/ch/reader/view_fixed_content.aspx?id=instructions
5. 投稿作者需提交投稿声明；专刊投稿文章不收审理费。录用刊发文章收取软件学报标准版面费。发表之后，将按软件学报标准支付稿酬，并赠送样刊。
6. 通过第一轮评审的论文作者，需在中国软件大会(ChinaSoft 2024) “形式化方法与应用”专刊论坛上做学术报告，根据论文修改情况和会议报告情况终审确定是否录用。

三、重要时间
收稿截稿日期：2024年8月26日
第一轮评审意见通知日期：2024年10月15日
提交修改稿日期：2024年10月30日
ChinaSoft 2024报告日期：2024年11月15-17日
终审结果通知日期：2024年12月2日
出版时间：2025年第8期