形式化方法以严格的数学化和机械化方法为基础来规约、设计、构建、验证、演进计算系统，是改善和确保计算系统质量的重要方法，其模型、技术和工具已成为安全攸关系统质量保障不可或缺的重要载体。
形式化方法己经成功应用于各种硬件设计，特别是芯片的设计。各大硬件制造商都有一个非常强大的形式化方法团队为保障系统的可靠性提供技术支持，例如IBM、AMD等等。近年来，随着形式验证技术和工具的发展，特别是在程序验证中的成功应用，形式化方法在处理软件开发复杂性和提高软件可靠性方面己显示出无可取代的潜力。各个著名的研究机构都投入了大量人力和物力从事这方面的研究。例如，美国宇航局（NASA）拥有一支庞大的形式化方法研究团队，他们在保证美国航天器控制软件正确性方面发挥了巨大作用，在美国研发“好奇号”火星探测器时，为了提高控制软件的可靠性和生产率，广泛使用了形式化方法。在新兴领域，如区块链及人工智能等领域，形式化方法也逐步应用适配，提升系统的整体安全可控。
ChinaSoft 2021形式化方法与应用Track特向关注该主题的研究人员公开征集稿件。本Track的主题将围绕形式化方法基础理论、技术、支持工具以及领域应用等。本Track将重点关注形式化方法在人工智能、区块链、量子计算等新兴领域内的研究成果，以及创新性理论技术在行业内的示范应用。
具有创新性和突破性的高水平研究成果将被邀请到ChinaSoft 2021报告。通过两轮评审、一次口头质询并达到《软件学报》发表要求的投稿论文，将在《软件学报》“形式化方法与应用”专刊发表。
一、征文范围
包括但不限于以下主题：
（1） 模型检验
（2） 硬件建模与验证
（3） 软件分析与验证
（4） 混成系统建模与验证
（5） 系统综合
（6） 运行时验证
（7） 定理证明
（8） 约束求解与判定过程
（9） 形式化工具及其评估
（10） 形式化方法应用案例
（11） 形式化方法与人工智能
（12） 形式化方法与区块链
（13） 形式化方法与量子计算
（14） 形式化方法与信息物理融合系统
（15） 形式化方法与安全
二、投稿要求和流程
1. 稿件格式：参照《软件学报》论文格式（网站上提供了论文模版，可下载）。
2. 投稿文章未在正式出版物上发表过，也不在其他刊物或会议的审稿过程中，不存在一稿多投现象；保证投稿文章的合法性(无抄袭、剽窃、侵权等不良行为)。
3. 投稿和评审方式：本Track投稿论文需经过两轮投稿和评审、一次口头报告和质询。
a) 第一轮：投稿使用ChinaSoft 2021会议系统（投稿链接https://easychair.org/conferences/?conf=chinasoft2021，选择“ChinaSoft 2021形式化方法与应用Track”），ChinaSoft 2021形式化方法与应用Track PC审稿，由会议通知评审结果，所有通过第一轮评审的稿件，进入第二轮；
b) 第二轮：按照第一轮评审专家的意见进行修改，修改稿采用“软件学报在线投稿系统”(http://www.jos.org.cn)进行投稿。投稿时请在备注栏中注明“形式化方法与应用”字样。第二轮投稿论文由期刊组织审稿，审稿意见由期刊通知，所有通过第二轮评审的稿件，进入第三轮；
c) 第三轮：要求稿件根据期刊评审意见修改论文，在ChinaSoft 2021会议进行口头报告，接受责任编辑的口头质询，责任编辑根据期刊评审结果、质询结果给出稿件处理建议，由期刊给出最终意见。
4. 投稿被录用后，由《软件学报》“形式化方法与应用”专刊发表。
三、重要日期
第一轮论文投稿截稿时间：2021年7月31日
第一轮审稿结果通知日期：2021年8月20日
第二轮论文修改稿提交日期：2021年9月5日
第二轮论文评审意见通知时间：2021年10月20日
第三轮论文报告时间：ChinaSoft 2021（2021年11月，西安）
第三轮论文修改稿提交日期：2021年12月10日
终审结果发出日期：2021年12月20日
最终稿提交日期：2021年12月31日
出版日期：2022年第8期
Track Chair：陈立前（国防科技大学）、孙猛（北京大学）
联系方式：lqchen@nudt.edu.cn
Track PC Members：
陈哲（南京航空航天大学）、邓玉欣（华东师范大学）、符鸿飞（上海交通大学）、甘庭（武汉大学）、贺飞（清华大学）、姜宇（清华大学）、 李国强（上海交通大学）、 李希萌（首都师范大学）、李樾（南京大学）、林望（浙江理工大学）、乔磊（北京控制工程研究所）、王竟亦（浙江大学）、熊英飞（北京大学）、许智武（深圳大学） 、薛白（中科院软件所）、 杨志斌（南京航空航天大学）、张立军（中科院软件所）、张民（华东师范大学）、 赵恒军（西南大学）、赵亮（西安电子科技大学）、 左志强（南京大学）