随着计算机系统在工业和生活中越来越广泛的应用，软件和硬件的可靠性受到越来越多的关注。定理证明方法将程序和系统的正确性表达为数学命题，然后使用逻辑推导的方式证明正确性。不同于基于程序测试的进路，定理证明方法能保证覆盖所有边缘情况，完全排除一个特定类型的错误。而基于逻辑推导的交互式定理证明技术还能不受系统状态空间大小的限制，验证非常复杂的系统和性质。因此，定理证明技术不仅是形式化方法领域，也是众多其他应用领域国内外学者的关注焦点和研究新热点。
近年来，定理证明已经逐步用于越来越多的软件、硬件系统验证，这一方面为软硬件系统的安全性保障提供了新的有力工具，另一方面也成为定理证明技术发展的有利契机。目前，定理证明的规模化问题、定理证明工具本身的底层逻辑理论问题、适应于定理证明方案的程序验证理论问题等变得越来越重要，对于分析、逻辑、概率等基础定理证明库或求解方案的需求也越来越迫切。
本Track“定理证明理论与应用”的主题将围绕定理证明本身的理论研究、定理证明本身的工具开发（特别是用于程序验证场景的工具开发）以及定理证明方法的各项应用，包括其在数学定理验证、算法数据结构验证、硬件验证、编译器验证、操作系统验证、区块链智能合约验证、概率、混成、量子等系统的建模以及机器学习的有关验证等各个方面的实际应用。定理证明及相关领域的突破性技术、关键理论、新验证工具以及重要应用将被邀请到ChinaSoft 2021做报告。通过两轮评审、一次口头质询并达到《软件学报》发表要求的投稿论文，将在《软件学报》“定理证明理论与应用”专刊发表。
一、征文范围
本专刊拟收录相关方向的综述或定理证明领域的突破性技术、关键理论、新验证工具以及重要应用。包括但不限于以下主题：
（1） 自动定理证明的理论和工具
（2） 交互式定理证明的理论和工具
（3） 形式化数学的验证及应用
（4） 基于定理证明的程序验证
（5） 信息安全相关的验证
（6） 算法与数据结构的验证及应用
（7） 硬件设计的建模和验证
（8） 编译器、操作系统设计与实现的验证
（9） 区块链智能合约和编程语言的建模和验证
（10） 机器学习算法和模型的验证
（11） 概率、混成、量子系统的建模和验证
（12） 机器学习在定理证明中的应用
二、投稿要求和流程
1. 稿件格式：参照《软件学报》论文格式（网站上提供了论文模版，可下载）。
2. 投稿要求：投稿文章未在正式出版物上发表过，也不在其他刊物或会议的审稿过程中，不存在一稿多投现象；保证投稿文章的合法性(无抄袭、剽窃、侵权等不良行为)。投稿文章如果有其作者开发的定理证明工具或者定理证明项目代码为佐证的，应当在投稿时一并提交相关代码的压缩包或者下载链接参与Artifact Evaluation。
3. 投稿和评审方式：本Track投稿论文需经过两轮投稿和评审、一次口头报告和质询。
a) 第一轮：投稿使用ChinaSoft 2021会议系统（投稿网站请见：https://easychair.org/conferences/?conf=chinasoft2021），ChinaSoft 2021定理证明理论与应用 Track PC审稿，由会议通知评审结果，所有通过第一轮评审的稿件，进入第二轮；
b) 第二轮：按照第一轮评审专家的意见进行修改，修改稿采用“软件学报在线投稿系统”(http://www.jos.org.cn)进行投稿。投稿时请在备注栏中注明“面向领域的软件系统构造与质量保障”字样。第二轮投稿论文由期刊组织审稿，审稿意见由期刊通知，所有通过第二轮评审的稿件，进入第三轮并参加Artifact Evaluation；
c) Artifact Evaluation：ChinaSoft 2021定理证明理论与应用 Track的Artifact Evaluation PC将对论文附带的定理证明工具、定理证明结果进行评审。
d) 第三轮：要求稿件根据期刊评审意见修改论文，在ChinaSoft 2021会议进行口头报告，接受责任编辑的口头质询，责任编辑根据期刊评审结果、质询结果给出稿件处理建议，由期刊给出最终意见。
三、重要日期
第一轮论文投稿截稿时间：2021年7月30日
第一轮审稿结果通知日期：2021年8月30日
第二轮论文修改稿提交日期：2021年9月15日
第二轮论文评审意见通知时间：2021年11月5日
Artifact Evaluation结果通知时间：2021年11月20日
第三轮论文报告时间：ChinaSoft 2021（2021年11月）
第三轮论文修改稿提交日期：2021年12月10日
终审结果发出日期：2021年12月20日
最终稿提交日期：2021年12月31日