抽象解释及其应用研究进展陈立前1范广生1,3尹帮虎2王戟1,31（国防科技大学计算机学院长沙410073）2（国防科技大学系统工程学院长沙410073）3（高性能计算国家重点实验室（国防科技大学）长沙410073）（lqchen@nudt.edu.cn）ResearchProgressonAbstractInterpretationandItsApplicationChenLiqian1,FanGuangsheng1,3,YinBanghu2,andWangJi1,31（CollegeofComputerScienceandTechnology,NationalUniversityofDefenseTechnology,Changsha410073）2（CollegeofSystemsEngineering,NationalUniversityofDefenseTechnology,Changsha410073）3（StateKeyLaboratoryofHighPerformanceComputing(NationalUniversityofDefenseTechnology),Changsha410073）AbstractAbstractinterpretationisatheoryofabstractionandapproximationofthemathematicalstructuresusedintheformaldescriptionofcomplexsystemsandtheinferenceorverificationoftheirproperties.Sincebeingproposedin1970s,abstractinterpretationhasbeenwidelyappliedtomanyfields,includingsemanticmodels,programanalysisandverification,verificationofhybridsystems,programtransformation,analysisofsystemsbiologymodels,etc.Inrecentyears,abstractinterpretationhasmadegreatprogressinprogramanalysis,neuralnetworkverification,completenessreasoning,improvementofabstractdomains,etc.Basedonthis,wesystematicallyreviewtheresearchprogressofabstractinterpretationanditsapplications.Firstly,weoutlinethebasicconceptsofabstractinterpretationtheory,andreviewtherecentresearchprogressofabstractinterpretationtheoryandabstractdomains;then,wereviewtherecentresearchprogressinabstractinterpretation-basedprogramanalysis,verificationandrobusttrainingofneuralnetworks,analysisofdeeplearningprograms;afterthat,wealsoreviewtheprogressofsomeotherapplicationsofabstractinterpretation,includingtrustworthinessassuranceofsmartcontract,informationsecurity,andquantumcomputing;Atlast,potentialfuturedirectionsinthefieldofabstractinterpretationarepointedout.Keywordsabstractinterpretation；programsemantics；programanalysis；formalverification；abstractdomain摘要抽象解释是一种对用于形式描述复杂系统行为的数学结构进行抽象和近似并推导或验证其...
