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

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

       投稿本Track的稿件通过两轮评审，将被邀请到ChinaSoft 2023做报告；通过两轮评审、一次口头质询并达到《软件学报》发表要求的投稿论文，将在《软件学报》“形式化方法与应用”专刊发表。

一、征文范围

包括但不限于以下主题：

1. 形式化方法理论、方法、技术与工具

（1）定理证明

（2）模型检测

（3）静态分析与运行时验证

（4）约束求解与判定

（5）规约与构造

（6）SMT与SAT求解

（7）模型驱动开发

（8）形式化方法中的机器学习与概率推理

（9）形式验证与仿真、测试的组合

（10）验证工具；

2. 面向特定应用的形式化方法

（1）可信人工智能

（2）区块链

（3）量子计算

（4）智能制造

（5）人机物融合系统

（6）软件的智能合成与验证

（7）芯片设计与软硬件协同

（8）信息安全与隐私。

二、投稿要求

1. 稿件格式：参照《软件学报》论文格式（网站上提供了论文模版，可下载）。

2. 投稿要求：

    (1) 投稿文章未在正式出版物上发表过，也不在其他刊物或会议的审稿过程中，不存在一稿多投现象；

    (2) 保证投稿文章的合法性(无抄袭、剽窃、侵权等不良行为)。

3. 投稿与评审方式：本Track投稿论文需经过两轮投稿和评审、一次口头报告和质询。

第一阶段：投稿使用ChinaSoft 2023会议系统（https://easychair.org/conferences/?conf=chinasoft2023），由ChinaSoft 2023形式化方法与应用Track PC审稿，由会议通知评审结果，所有通过第一轮评审的稿件。

第二阶段：按照第一轮评审专家的意见进行修改，修改稿采用“软件学报在线投稿系统”(http://www.jos.org.cn)进行投稿。投稿时请在备注栏中注明“形式化方法与应用”字样。第二轮投稿论文由期刊组织审稿，审稿意见由期刊通知，所有通过第二轮评审的稿件。

第三阶段：要求稿件根据期刊评审意见修改论文，在ChinaSoft 2023会议进行口头报告，接受责任编辑的口头质询，责任编辑根据期刊评审结果、质询结果给出稿件处理建议，由期刊给出最终意见。

三、重要日期

第一阶段：ChinaSoft会议投稿

    论文投稿截稿时间：2023年7月31日

    审稿结果通知日期：2023年8月31日

第二阶段：软件学报在线投稿

    论文修改稿提交截止时间：2023年9月11日

    论文评审意见通知时间：2023年11月1日

第三阶段：ChinaSoft 2023 评审

    论文修改稿提交截止时间：2023年11月16日

    ChinaSoft2023报告日期：2023年12月1-3日

终审结果发出日期：2023年12月18日

出版时间：2024年第9期

四、特约编辑

曹钦翔，上海交通大学，[email protected]

宋富，上海科技大学，[email protected]

詹乃军，中国科学院软件研究所，[email protected]