静态程序分析方法和工具

Static Program Analysis Methods and Tools

综述静态程序分析的方法和工具。采用系统化文献评价方法和文献计量分析方法,通过论文的收集、筛选、内容提取等过程,对大量论文的信息进行总结分析。通过文献管理工具Endnote、数据分析软件SPSS和文献分析工具Ref Viz,统计分析论文数据库的基本信息,包括年代分布、作者分布、关键词和热点分析。通过阅读大量相关论文,静态程序分析方法可分为模型检测、符号执行、定理证明、抽象解释等。静态程序分析工具包括形式化验证工具、模型检测工具等。最后,总结静态分析方法和工具的不足。

Reviews the static program analysis methods and tools. Uses systematic literature review method and bibliometric analysis method, to analyze and summarize the information in a large of papers by collecting, screening and extracting content of papers. Through Endnote, SPSS,and Ref Viz, the basic information in papers database is added up and analyzed, including age distribution, author distribution, keywords and hotspot analysis. By reading a large number of papers, static program analysis methods can be divided into model checking, symbolic execution, theorem proving, abstract interpretation, etc. Static program analysis tools include formal verification tools, model checking tools and so on. At last, summarizes the shortcomings of static analysis methods and tools.