软件发展的核心问题之一是如何保证软件系统安全可靠。如今，硬件运算速度变得越来越快、体系结构变得越来越复杂，软件的功能也变得越来越强大而复杂，如何开发可靠的软件系统，已经成为一项巨大的挑战。特别是现在计算机系统已广泛应用于许多关系国计民生的安全攸关系统中，例如高速列车控制系统、航空航天控制系统、核反应堆控制系统等等，这些系统中的任何错误都可能导致灾难性后果。目前，形式化方法已经成功应用于各种硬件设计，特别是芯片的设计。各大硬件制造商都有一个非常强大的形式化方法团队为保障系统的可靠性提供技术支持，例如IBM、AMD等等。同时，随着形式验证技术（如定理证明、模型检验等）的发展，形式化方法在提高软件可靠性方面已显示出无可取代的潜力。各个著名的研究机构都投入了大量人力和物力从事这方面的研究。例如，美国宇航局（NASA）拥有一支庞大的形式化方法研究团队，他们在保证美国航天器控制软件正确性方面发挥了巨大作用，在美国研发“好奇号”火星探测器时，为了提高控制软件的可靠性和生产率，广泛使用了形式化方法。在新兴领域，如区块链及人工智能等领域，形式化方法也逐步应用适配，提升系统的整体安全可控。

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

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

专刊题目：形式化方法与应用
特约编辑：曹钦翔（上海交通大学）宋富（上海科技大学）詹乃军（中国科学院软件研究所）
出版时间：2024年第9期

一、征文范围
包括但不限于以下主题：
1. 形式化方法理论、方法、技术与工具
（1）定理证明
（2）模型检测
（3）静态分析与运行时验证
（4）约束求解与判定
（5）规约与构造
（6）SMT与SAT求解
（7）模型驱动开发
（8）形式化方法中的机器学习与概率推理
（9）形式验证与仿真、测试的组合
（10）验证工具
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. 通过第一轮评审的论文作者，需在ChinaSoft2023上做学术报告，根据论文修改情况和会议报告情况终审确定是否录用。

三、重要时间
收稿截稿时间：2023年9月11日
第一轮评审意见通知时间：2023年11月1日
提交修改稿时间：2023年11月16日
ChinaSoft2023会议时间：2023年12月1日–3日
最终结果通知时间：2023年12月18日
出版时间：2024年第9期