随着计算机系统在工业和生活中越来越广泛的应用，软件和硬件的可靠性受到越来越多的关注。形式化方法使用严格的数学语言对计算机系统建模，并在计算机的辅助下验证系统的正确性。与测试不同，形式化方法可以完全排除某些类型的错误。约束求解和定理证明是形式化方法中的两大关键技术。在约束求解方面，SAT和SMT求解器已经在学术界和工业界得到了广泛应用，比如SAT求解器用于EDA领域的等价性验证，SMT求解器用于程序验证和白盒模糊测试等。交互式定理证明通过人和计算机之间的交互完成证明，能够验证非常复杂的系统和性质，例如编译器和操作系统的正确性验证。约束求解与定理证明专刊关注约束求解和定理证明的理论、技术、工具与应用，包括在EDA、符号执行、模型检测、程序分析与验证、系统安全等领域的应用。
ChinaSoft 2022约束求解与定理证明Track征集国内外相关研究人员在约束求解和定理证明的理论和应用等方面取得的重大突破和具有创新性、影响力的高水平研究成果，为相关研究者和实践者提供发表最新成果的学术交流平台。本Track将面向以下几个研究方向（不限于此）征文：1) SAT和SMT求解；2) 分离逻辑、时序逻辑等逻辑系统的约束求解；3) 交互式定理证明理论和工具；4) 形式化数学；5) 程序验证、硬件和操作系统的验证；6) 约束求解和定理证明的其他应用。
具有创新性和突破性的高水平研究成果将被邀请到ChinaSoft 2022报告。通过两轮评审、一次口头质询并达到《软件学报》发表要求的投稿论文，将在《软件学报》“约束求解与定理证明”专刊发表。
一、征文范围
包括但不限于以下主题：
(1) SAT求解
(2) SMT求解
(3) 交互式定理证明理论和工具
(4) 形式化数学验证
(5) 其他逻辑（比如分离逻辑和时序逻辑等）理论与工具
(6) 约束求解和定理证明的应用
二、投稿要求和流程
1. 稿件格式：参照《软件学报》论文格式(《软件学报》网站（http://www.jos.org.cn/jos/home）上提供了论文模版，可下载)。
2. 来稿内容应属于作者的科研成果，数据真实、可靠，未公开发表过；引用他人成果已注明出处；署名无争议；是有创新学术见解的研究成果的完整论述，对该学术领域的发展有积极意义。
3. 论文语言流畅，可读性强，表述清楚、有条理，无逻辑、语法错误，审稿人审理时无阅读、理解障碍。
4. 投稿和评审方式：本Track投稿论文需经过两轮投稿和评审、一次口头报告和质询。
（1） 第一轮：投稿使用ChinaSoft 2022会议系统（投稿链接https://easychair.org/conferences/?conf=chinasoft2022，选择“约束求解与定理证明”Track），由ChinaSoft 2022约束求解与定理证明Track PC审稿，由会议通知评审结果，所有通过第一轮评审的稿件，进入第二轮；
（2） 第二轮：按照第一轮评审专家的意见进行修改，修改稿采用“软件学报在线投稿系统”(http://www.jos.org.cn)进行投稿。投稿时请在备注栏中注明“约束求解与定理证明”字样。第二轮投稿论文由期刊组织审稿，审稿意见由期刊通知，所有通过第二轮评审的稿件，进入第三轮；
（3） 要求稿件根据期刊评审意见修改论文，在ChinaSoft 2022会议进行口头报告，接受责任编辑的口头质询，责任编辑根据期刊评审结果、质询结果给出稿件处理建议，由期刊给出最终意见。
5. 投稿被录用后，由《软件学报》“约束求解与定理证明”专刊发表。
三、重要日期
(1) 第一阶段：ChinaSoft会议投稿
1） ChinaSoft 会议论文截稿时间：2022年7月15日（延期到2022年7月31日），投稿中选择“约束求解与定理证明”Track
2） 审稿结果通知日期：2022年8月20日（延期到2022年8月25日）
(2) 第二阶段：期刊专刊投稿
1） 专刊论文提交截止日期：2022年9月5日
2） 专刊论文审稿结果通知日期：2022年10月20日
(3) 第三阶段：会议报告及修改提交
1）专刊论文修改稿提交日期：2022年10月30日
2）会议日期：2022年11月，上海
3）终审结果通知日期：2022年12月20日
4）最终录用稿提交日期：2023年1月5日
5）专刊出版日期：2023年第8期
四、 Track Chairs
蔡少伟（中国科学院软件研究所）
陈振邦（国防科技大学）
王戟（国防科技大学）
詹博华（中国科学院软件研究所）
赵永望（浙江大学）
五、 Track PC Members
卜磊（南京大学）
曹钦翔（上海交通大学）
陈钢（南京航空航天大学）
陈海波（上海交通大学））
邓益平（华为）
邓玉欣（华东师范大学）
冯新宇（南京大学）
顾荣辉（哥伦比亚大学）
贺飞（清华大学
侯哲（澳大利亚Griffith University）
梁红瑾（南京大学）
李建文（华东师范大学）
刘江（中国科学院重庆绿色智能技术研究院）
刘万伟（国防科技大学）
罗川（北京航空航天大学）
马菲菲（中科院软件所）
施智平（首都师范大学）
宋富（上海科技大学）
孙猛（北京大学）
邵中（耶鲁大学）
田聪（西安电子科技大学）
王生原（清华大学）
吴贯锋（西南交通大学）
吴志林（中科院软件所）
熊英飞（北京大学）
张弘策（香港科技大学（广州））
张健（中科院软件所）
张兴元（解放军理工学院）
张羽丰（湖南大学）