摘要
目前提高软件可靠性的方法有3种:动态测试、静态分析和程序验证。动态测试的结果依赖于测试集的设计,误报率低,漏报率高,分析结果不稳定。程序验证可以对程序的各种性质进行完备的验证。但目前程序验证通常都需要手动证明,分析成本最高。而程序静态分析可以更早、更全面、较高效和低成本地检测到程序中的缺陷。其中符号执行技术是一种比较有应用前景的静态分析技术,可以很好地控制精确度。针对符号执行可伸缩性差和容易产生路径爆炸的问题,在符号执行过程中利用形状分析技术实现自动推导循环不变式和构建函数行为规范,实现了一个较为实用的C程序分析工具。
Dynamic testing,static analysis and formal verification are three major methods for improving the dependability of software.Since the result of dynamic testing depends on the design of test case suite,it is unstable and can lead to high false negative rate.Formal verification is a complementary method for proving the correctness of software.So far most of the proof still need to be implemented by hand which makes formal verification hard with high cost.Static analysis is an efficient and low-cost method for detecting bugs in software.One of the promising techniques of static analysis is symbolic execution,while it has a good control over the degree of accuracy.Targeting at the path explosion problem and poor scalability of symbolic execution,and taking advantage of shape analysis,loop invariants and function specification inference during symbolic execution,we implemented an efficient analysis tool for C programs.
出处
《计算机科学》
CSCD
北大核心
2016年第3期193-198,共6页
Computer Science
基金
国家自然科学基金面上项目(61170018)资助
关键词
符号执行
静态分析
循环不变式
递归函数
Symbolic execution
Static analysis
Loop invariant
Recursive function
