基于抽象解释的迹划分技术研究
    点此下载全文
引用本文:张 弛,丁泽文,刘林武.基于抽象解释的迹划分技术研究[J].计算技术与自动化,2017,(4):88-92
摘要点击次数: 872
全文下载次数: 0
作者单位
张 弛,丁泽文,刘林武 (南京航空航天大学 计算机与技术学院,江苏 南京 211106) 
中文摘要:确保程序中没有运行时错误,对于软件安全性的保证十分重要。基于抽象解释的静态分析方法对程序语义进行抽象,是验证运行时错误最合适的形式化方法之一。然而抽象解释对于程序语义的抽象可能导致过近似问题,从而引发误报,降低了分析精度。因此提出了迹划分的技术,根据程序的迹对程序控制流图进行划分,对静态分析过程进行局部细化,减少了抽象解释过程中过近似引发的误报。迹划分技术以局部分析效率降低为代价换来了分析精度的提高。
中文关键词:抽象解释  迹划分  静态分析  运行时错误  软件安全性
 
Research on Trace Partitioning Based on Abstract Interpretation
Abstract:Ensuring the absence of run-time errors in the program is important for the software safety.The program semantics was abstracted by the static analysis method based on abstract interpretation.It is the most appropriate formal method for validating run-time errors.However,the over-approximation of program semantics by the abstract interpretation may lead to false alarms,which reduce the accuracy of analysis.So the technology of trace partitioning was proposed.The control-flow-graph was partitioned according to the trace,and then the process of static analysis can be local refinement.The method reduced the false alarms caused by over-approximation.Trace partitioning obtains higher analytical accuracy at the cost of reduction of local analysis efficiency.
keywords:abstract interpretation  trace partitioning  static analysis  run-time error  software safety
查看全文   查看/发表评论   下载pdf阅读器