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

Research Progress on Abstract Interpretation and Its Application

作　　者：陈立前[1] 范广生 尹帮虎 王戟[1,3] Chen Liqian;Fan Guangsheng;Yin Banghu;Wang Ji(College of Computer Science and Technology,National University of Defense Technology,Changsha 410073;College of Systems Engineering,National University of Defense Technology,Changsha 410073;State Key Laboratory of High Performance Computing(National University of Defense Technology),Changsha 410073)

机构地区：[1]国防科技大学计算机学院,长沙410073 [2]国防科技大学系统工程学院,长沙410073 [3]高性能计算国家重点实验室国防科技大学,长沙410073

出　　处：《计算机研究与发展》2023年第2期227-247,共21页Journal of Computer Research and Development

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

摘　　要：抽象解释是一种对用于形式描述复杂系统行为的数学结构进行抽象和近似并推导或验证其性质的理论.抽象解释自20世纪70年代提出以来,在语义模型、程序分析验证、混成系统验证、程序转换、系统生物学模型分析等领域取得了广泛应用.近年来,抽象解释在程序分析、神经网络验证、完备性推理、抽象域改进等方面取得较大进展.基于此,系统综述了抽象解释及其应用的研究进展.首先概述了抽象解释理论的基本概念,介绍了抽象解释理论、抽象域的研究进展;然后概述了基于抽象解释的程序分析方面的研究进展;之后概述了基于抽象解释的神经网络模型验证、神经网络模型鲁棒训练、深度学习程序的分析等方面的研究进展;又对抽象解释在智能合约可信保证、信息安全保证、量子计算可信保证等方面的应用进展进行了介绍;最后指明了抽象解释未来可能的研究方向.interpretation is a theory of abstraction and approximation of the mathematical structures used in the formal description of complex systems and the inference or verification of their properties.Since being proposed in 1970 s,abstract interpretation has been widely applied to many fields,including semantic models,program analysis and verification,verification of hybrid systems,program transformation,analysis of systems biology models,etc.In recent years,abstract interpretation has made great progress in program analysis,neural network verification,completeness reasoning,improvement of abstract domains,etc.Based on this,we systematically review the research progress of abstract interpretation and its applications.Firstly,we outline the basic concepts of abstract interpretation theory,and review the recent research progress of abstract interpretation theory and abstract domains;then,we review the recent research progress in abstract interpretation-based program analysis,verification and robust training of neural networks,analysis of deep learning programs;after that,we also review the progress of some other applications of abstract interpretation,including trustworthiness assurance of smart contract,information security,and quantum computing;At last,potential future directions in the field of abstract interpretation are pointed out.

关 键 词：抽象解释 程序语义 程序分析 形式验证 抽象域 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]