结合抽象解释与可满足性模理论的数值程序分析

No matter the traditional scientific computing software or the nowadays cyber-physical systems software, all depend a lot on the background mathematical or physical model, and thus involve plenty much of numerical computation in their source code. Moreover, many kinds of numerical intensive software play an important role in safety-critical fields, which suggests the importance of their dependability. This project aims to develop advanced numerical program analysis techniques by combining abstract interpretation and Satisfiability Modulo Theories (SMT), to exploit the complementary advantages of both theories. More specially, this project focuses on four aspects: (1) Symbolic encoding of program semantics via SMT; (2) Numerical abstraction for SMT Formula; (3) Block-wise program analysis framework based on numerical abstract domains and SMT, as well as its optimization; (4) The application of the proposed approach on numerical intensive software in real-world systems. On this basis, an automatic numerical static analyzer will be developed in this project, which will show its effectiveness on numerical intensive software in the fields like aerospace, avionics, scientific computing, etc. This project will advance the development of the research on software analysis and verification, and contribute to dependability assurance of numerical intensive software.

无论是传统的科学计算软件，还是新型的信息物理融合软件，由于与数学或物理模型紧密相关，软件代码中往往包含大量数值运算。且很多数值密集型软件往往在安全攸关领域中承载着重要使命，其可信性至关重要。抽象解释和可满足性模理论(SMT)都擅长处理数值，但各具优缺点。本项目拟结合抽象解释与SMT来研究新的数值程序分析技术，旨在将两者有机融合，取长补短，实现优势互补，提升整体分析效果。具体研究内容包括：(1)基于SMT的程序语义符号化编码技术；(2)面向SMT公式的数值抽象技术；(3)基于数值抽象域与SMT的块级程序分析框架及优化；(4)方法在数值密集型软件分析中的应用研究。在此基础上，开发自动化程度较高的数值程序分析工具，并针对航天航空、科学计算等领域数值密集型软件进行示范应用。本项目的研究将对软件分析与验证相关方向研究起到促进作用，对数值密集型软件的可信保障具有重要实际应用价值。

计算机程序中的许多性质和常见错误（如算术溢出、计算精度缺陷等），与程序中数值型变量及其上的数值运算密切相关。针对数值程序开展自动分析，对于提高数值密集型安全攸关软件的可信性具有重要意义。抽象解释和可满足性模理论(SMT)都擅长处理数值，但各具优缺点。本项目结合抽象解释与SMT来研究新的数值程序分析技术，以提升整体分析效果。. 经过四年的研究，项目组依据计划，完成了各项研究内容，达到了预期的研究目标。在数值抽象域设计与实现、结合数值抽象域与SMT、数值程序分析技术、数值程序分析应用等方面形成了较为系统、深入的研究成果，在基准测试程序和航天领域嵌入式代码上的实验和应用验证了项目成果的有效性。进展要点如下：1)在抽象域研究方面，设计实现了线性绝对值等式抽象域、正负两区间抽象域等非凸数值抽象域；2)在结合数值抽象域与SMT研究方面，设计实现了结合数值抽象域与SMT的数值程序工具原型，支持不变式的生成和程序中数值相关运行时错误的检测；3)在数值程序分析技术研究方面，提出了基于层次化分析的数值不变式生成优化技术、基于迭代抽象测试的数值程序验证等新技术；4)在数值程序分析应用研究方面，提出了基于符号传播的神经网络鲁棒性验证增强技术、基于迭代抽象分析的神经网络安全性质验证方法、基于抽象解释的神经网络架构程序数值缺陷检测方法、基于条件数指导的浮点程序精度缺陷检测方法、基于数学近似的浮点程序精度缺陷修复方法、基于数值抽象的程序资源使用量自动分析方法。. 项目执行期间，共发表学术论文20篇，其中CCF A类4篇，CCF B类 8篇，CCF C类2篇。部分论文发表在TCAD、POPL 2019、FSE 2020、ASE 2022等程序语言、软件工程与嵌入式系统领域的重要国际期刊会议上，其中发表在FSE 2020上的论文获得ACM SIGSOFT杰出论文奖，发表在软件学报上的论文获得《软件学报》2021年高影响力论文。申请国家发明专利6项（其中，授权2项），并形成了若干软件工具原型，其中一项工具原型获NASAC 2019软件研究成果原型系统竞赛（命题型）二等奖，部分工具原型在Github社区开源。项目负责人于2020年获北京市科技进步一等奖1项。项目共培养博士2名、硕士5名。