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

本专刊围绕形式化方法基础理论、技术、支撑工具以及领域应用等，重点关注形式化方法与理论计算机科学、软件工程、系统软件（特别是异构多核环境下的分布式实时操作系统、泛在操作系统等）、嵌入式系统、人机物融合系统、网络与信息安全、可信人工智能（智能制造、智能交通、智能控制、可信机器学习）等领域的交叉结合。拟收录相关方向的综述或突破性的关键技术、关键理论、以及得到工业应用的工具等相关论文。

经过第一轮评审的论文作者需要参加ChinaSoft2022会议并到会报告，之后特约编辑和编辑部根据复审情况和会议报告情况决定文章的最终结果，专刊将在2023年第7期出版。读者群体包括形式化方法、系统软件、嵌入式系统、人机物融合系统等多个领域的研究人员和工程人员。

专刊题目：形式化方法与应用
特约编辑：董云卫（西北工业大学）刘关俊（同济大学）毛晓光（国防科技大学）
出版时间：2023年第7期

一、征文范围
包括但不限于以下主题：
1. 形式化方法与技术

(1)       模型检测；

(2)       定理证明；

(3)       静态分析与运行时验证；

(4)       约束求解与判定过程；

(5)       规约与细化；

(6)       SMT与SAT求解；

(7)       模型驱动开发；

(8)       形式化方法中的机器学习与概率推理；

(9)       形式化方法与仿真、测试的组合；

(10)   形式化方法支撑工具。

2. 形式化方法的工程应用

(1)       形式化方法与可信人工智能；

(2)       形式化方法与区块链；

(3)       形式化方法与量子计算；

(4)       形式化方法与智能制造；

(5)       形式化方法与人机物融合系统；

(6)       形式化方法与（泛在）操作系统；

(7)       形式化方法与混成系统；

(8)       形式化方法与软硬件协同；

(9)       形式化方法与软件智能合成；

(10)   形式化方法与隐私、安全。

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

三、重要时间
截稿时间：2022年9月5日

第一轮评审意见通知时间：2022年10月20日

提交修改稿时间：2022年10月30日

ChinaSoft2022报告日期：2022年11月25–27日

终审结果发出日期：2022年12月20日

最终稿提交日期：2023年1月5日

出版时间：2023年第7期