夜雨聆风形式化方法以严格的数学化和机械化方法为基础来规约、设计、构建、验证、演进计算系统，是改善和确保计算系统质量的重要方法，其模型、技术和工具已成为安全攸关系统质量保障不可或缺的重要载体。形式化方法已经成功应用于各种硬件（如芯片）的设计，各大硬件制造商（如IBM、AMD等）都有一支强大的形式化方法团队，为保障系统的可靠性提供技术支持。近年来，随着形式验证技术和工具的发展，特别是在程序验证中的成功应用，形式化方法在处理软件开发复杂性和提高软件可靠性方面已显示出无可取代的潜力。著名的研究机构都投入了大量人力和物力从事这方面的研究。例如，美国宇航局（NASA）拥有一支庞大的形式化方法研究团队，在保障美国航天器控制软件正确性方面发挥了巨大作用；又如，中国航天科技集团公司五院自主研发的航天操作系统SpaceOS、华为自主研发的鸿蒙操作系统HarmonyOS等，均使用了形式化方法，从根本上确保系统设计的无差错和高可靠。在新兴领域，如区块链、可信人工智能等领域，形式化方法也逐步应用适配，提升系统的整体安全可控；最近，形式化方法与生成式人工智能的交叉结合也受到广泛关注。
本专刊围绕形式化方法基础理论、技术、支撑工具及领域应用，重点关注形式化方法与理论计算机科学、编程语言、软件工程、基础软件（操作系统、编译器、电子自动化设计等）、实时嵌入式系统、人机物融合系统、概率/量子系统、网络与信息安全、可信人工智能（可信机器学习、智能制造、智能交通、智能控制）、生成式人工智能等领域的交叉结合。拟收录相关方向的综述或突破性的关键理论、关键技术以及得到工业应用的工具等相关论文。
经过第一轮评审的论文作者需要参加ChinaSoft2026会议并到会报告，之后特约编辑和编辑部根据复审情况和会议报告情况决定文章的最终结果，专刊将在2027年第9期出版。读者群体包括形式化方法、软件工程、嵌入式系统、可信人工智能等多个领域的研究人员和工程人员。
专刊题目：形式化方法与应用
特约编辑：陈宇奇（上海科技大学）、李国强（上海交通大学）、田聪（西安电子科技大学）
截稿时间：2026年8月17日
出版时间：2027年第9期
