NASAC+FMAC2020 形式化方法与应用专刊征文通知-CCF 2020 中国软件大会

NASAC+FMAC2020 形式化方法与应用专刊征文通知

计算机科学的发展主要涉及硬件和软件的发展，而软、硬件发展的核心问题之一是如何保证它们是安全可靠的。如今，硬件性能变得越来越高，运算速度变得越来越快，体系结构变得越来越复杂，软件的功能也变得越来越复杂，如何开发可靠的软、硬件系统，己经成为计算机科学发展的巨大挑战。特别是现在计算机系统广泛应用于许多安全攸关系统中，如高速列车控制系统、航空航天控制系统、核反应堆控制系统、医疗设备控制系统等等，这些系统中的任何错误都可能导致灾难性后果。

形式化方法己经成功应用于各种硬件设计，特别是芯片的设计。各大硬件制造商都有一个非常强大的形式化方法团队为保障系统的可靠性提供技术支持，例如IBM、AMD等等。近年来，随着形式验证技术和工具的发展，特别是在程序验证中的成功应用，形式化方法在处理软件开发复杂性和提高软件可靠性方面己显示出无可取代的潜力。各个著名的研究机构都投入了大量人力和物力从事这方面的研究。例如，美国宇航局（ＮＡＳＡ）拥有一支庞大的形式化方法研究团队，他们在保证美国航天器控制软件正确性方面发挥了巨大作用，在美国研发“好奇号”火星探测器时，为了提高控制软件的可靠性和生产率，广泛使用了形式化方法。在新兴领域，如区块链及人工智能等领域，形式化方法也逐步应用适配，提升系统的整体安全可控。

本专刊重点关注形式化基础方法、技术、支持工具以及领域交叉应用等。将收录国内外在解决难题和挑战过程所取得的理论、技术或实验等方面创新性、突破性的高水平研究成果，并探讨其在产业界的应用前景。读者群体包括形式化方法、数理逻辑、系统软件、软件工程及相关领域的研究人员、DevOps全栈工程师、专业软件工程师等。

专刊题目：形式化方法与应用

特约编辑：田聪（西安电子科技大学）邓玉欣（华东师范大学）姜宇（清华大学）

出版时间：2021年第6期

一、征文范围

征文范围（包括但不限于以下主题）

模型检验算法和工具；
系统综合算法和工具；
程序分析和软件验证；
形式化方法与机器学习；
形式化方法与区块链；
形式化方法与量子计算；
形式化方法与信息物理融合系统；
混成系统建模与验证技术；
硬件建模与验证技术；
嵌入式软件分析验证；
概率模型检测；
运行时验证；
组合验证；
并行程序分析验证；
形式化方法与安全；
生物系统的形式化模型和分析；
工业系统的形式化分析；
符号执行；

二、投稿要求和流程

1. 投稿方式：采用“软件学报在线投稿系统”(http://www.jos.org.cn)投稿。投稿时请选择投稿类型为"专刊投稿"，并在文章标题+”形式化方法与应用”字样。

软件学报在线投稿系统

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

3. 投稿文章未在正式出版物上发表过，也不在其他刊物或会议的审稿过程中，不存在一稿多投现象；保证投稿文章的合法性(无抄袭、剽窃、侵权等不良行为)。

4. 其他事项请参阅投稿指南： http://www.jos.org.cn/jos/ch/reader/view_fixed_content.aspx?id=instructions

投稿指南

5. 投稿作者需提交投稿声明；专刊投稿文章不收审理费。录用刊发文章收取软件学报标准版面费。发表之后，将按软件学报标准支付稿酬，并赠送样刊。

6. 通过阶段评审的论文，需在2020年CCF系统软件专委会、软件工程专委会、形式化方法专委会承办的 NASAC+FMAC 2020（2020年11月，重庆）上做学术报告，根据论文修改情况和会议报告情况终审确定是否录用。

三、重要日期

论文截稿时间：2020年8月30日
评审意见通知时间：2020年10月20日
NASAC+FMAC 2020报告时间：2020年11月（重庆）
论文修改稿提交日期：2020年12月10日
终审结果发出日期：2020年12月20日
最终稿提交日期：2020年12月31日
出版日期：2021年第6期
四、特邀编委联系

四、特邀编委联系

田聪（西安电子科技大学）

ctian@mail.xidian.edu.cn

邓玉欣（华东师范大学）

yxdeng@sei.ecnu.edu.cn

姜宇（清华大学）

jiangyu198964@126.com