抽象解释及其应用研究进展

作     者：陈立前 范广生 尹帮虎 王戟 Chen Liqian;Fan Guangsheng;Yin Banghu;Wang Ji

作者机构：国防科技大学计算机学院长沙410073 国防科技大学系统工程学院长沙410073 高性能计算国家重点实验室国防科技大学长沙410073 

出 版 物：《计算机研究与发展》 (Journal of Computer Research and Development)

年 卷 期：2023年第60卷第2期

页      面：227-247页

核心收录：

学科分类：081203[工学-计算机应用技术] 08[工学] 0835[工学-软件工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家重点研发计划项目(2022YFA1005101) 国家自然科学基金项目(61872445,62032024,62102432) 湖南省自然科学基金项目(2021JJ40697) 

主　　题：抽象解释 程序语义 程序分析 形式验证 抽象域 

摘      要：抽象解释是一种对用于形式描述复杂系统行为的数学结构进行抽象和近似并推导或验证其性质的理论.抽象解释自20世纪70年代提出以来,在语义模型、程序分析验证、混成系统验证、程序转换、系统生物学模型分析等领域取得了广泛应用.近年来,抽象解释在程序分析、神经网络验证、完备性推理、抽象域改进等方面取得较大进展.基于此,系统综述了抽象解释及其应用的研究进展.首先概述了抽象解释理论的基本概念,介绍了抽象解释理论、抽象域的研究进展;然后概述了基于抽象解释的程序分析方面的研究进展;之后概述了基于抽象解释的神经网络模型验证、神经网络模型鲁棒训练、深度学习程序的分析等方面的研究进展;又对抽象解释在智能合约可信保证、信息安全保证、量子计算可信保证等方面的应用进展进行了介绍;最后指明了抽象解释未来可能的研究方向.