随着计算机系统在工业和生活中越来越广泛的应用,软件和硬件的可靠性受到越来越多的关注。形式化方法使用严格的数学语言对计算机系统建模,并在计算机的辅助下验证系统的正确性。与测试不同,形式化方法可以完全排除某些类型的错误。约束求解和定理证明是形式化方法中的两大关键技术。在约束求解方面,SAT和SMT求解器已经在学术界和工业界得到了广泛应用,比如SAT求解器用于EDA领域的等价性验证,SMT求解器用于程序验证和白盒模糊测试等。交互式定理证明通过人和计算机之间的交互完成证明,能够验证非常复杂的系统和性质,例如编译器和操作系统的正确性验证。约束求解与定理证明专刊关注约束求解和定理证明的理论、技术、工具与应用,包括在EDA、符号执行、模型检测、程序分析与验证、系统安全等领域的应用。
本专刊征集国内外相关研究人员在约束求解和定理证明的理论和应用等方面取得的重大突破和具有创新性、影响力的高水平研究成果,为相关研究者和实践者提供发表最新成果的学术交流平台。本专刊将面向以下几个研究方向(不限于此)征文:1) SAT和SMT求解;2) 分离逻辑、时序逻辑等逻辑系统的约束求解;3) 交互式定理证明理论和工具;4) 形式化数学;5) 程序验证、硬件和操作系统的验证;6) 约束求解和定理证明的其他应用。
经过第一轮评审的论文作者需要参加ChinaSoft 2022会议并到会报告,之后特约编辑和编辑部根据复审情况和会议报告情况决定文章的最终结果,专刊将在2023年第8期出版。读者群体包括形式化方法、软件工程、系统软件、硬件设计等多个领域的研究人员和工程人员。
专刊题目:约束求解与定理证明
特约编辑:蔡少伟(中国科学院软件研究所)陈振邦(国防科技大学)王戟(国防科技大学)詹博华(中国科学院软件研究所)赵永望(浙江大学)
出版时间:2023年第8期
一、征文范围
包括但不限于以下主题:
(1) SAT求解
(2) SMT求解
(3) 交互式定理证明理论和工具
(4) 形式化数学验证
(5) 其他逻辑(比如分离逻辑和时序逻辑等)理论与工具
(6) 约束求解和定理证明的应用
二、投稿要求
1. 投稿方式:采用“软件学报在线投稿系统”(http://www.jos.org.cn)投稿。投稿时请选择投稿类型为“专刊投稿”,并在备注栏中注明“约束求解与定理证明”字样。
2. 稿件格式:参照《软件学报》论文格式(网站上提供了论文模版,可下载)。
3. 投稿文章未在正式出版物上发表过,也不在其他刊物或会议的审稿过程中,不存在一稿多投现象;保证投稿文章的合法性(无抄袭、剽窃、侵权等不良行为)。
4. 其他事项请参阅投稿指南http://www.jos.org.cn/ch/reader/view_fixed_content.aspx?id=instructions
5. 投稿作者需提交投稿声明;专刊投稿文章不收审理费。录用刊发文章收取软件学报标准版面费。发表之后,将按软件学报标准支付稿酬,并赠送样刊。
6. 通过第一轮评审的论文作者,需在ChinaSoft 2022上做学术报告,根据论文修改情况和会议报告情况终审确定是否录用。
三、重要时间
截稿时间:2022年9月5日
第一轮评审意见通知时间:2022年10月20日
提交修改稿时间:2022年10月30日
ChinaSoft2022报告日期:2022年11月25–27日
终审结果发出日期:2022年12月20日
最终稿提交日期:2023年1月5日
出版时间:2023年第8期