计算机科学 ›› 2016, Vol. 43 ›› Issue (3): 193-198.doi: 10.11896/j.issn.1002-137X.2016.03.036
梁家彪,李兆鹏,朱玲,沈咸飞
LIANG Jia-biao, LI Zhao-peng, ZHU Ling and SHEN Xian-fei
摘要： 目前提高软件可靠性的方法有3种:动态测试、静态分析和程序验证。动态测试的结果依赖于测试集的设计,误报率低,漏报率高,分析结果不稳定。程序验证可以对程序的各种性质进行完备的验证。但目前程序验证通常都需要手动证明,分析成本最高。而程序静态分析可以更早、更全面、较高效和低成本地检测到程序中的缺陷。其中符号执行技术是一种比较有应用前景的静态分析技术,可以很好地控制 精确度。针对符号执行可伸缩性差和容易产生路径爆炸的问题,在符号执行过程中利用形状分析技术实现自动推导循环不变式和构建函数行为规范,实现了一个较为实用的C程序分析工具。
| [1] Hoare C A R.An axiomatic basis for computer programming[J].Communications of the ACM,1969,12(10):576-580 [2] Reynolds J C.Separation logic:A logic for shared mutable data structures[C]∥17th Annual IEEE Symposium on Logic in Computer Science,2002.IEEE,2002:55-74 [3] Clarke E M,Emerson E A.Design and synthesis of synchronization skeletons using branching time temporal logic[M].Springer Berlin Heidelberg,1982 [4] Kildall G A.A unified approach to global program optimization[C]∥Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages.ACM,1973:194-206 [5] Cousot P,Cousot R.Interpretation:a unified lattice model forstatic analysis of programs by construction or approximation of fixpoints[C]∥Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages.ACM,1977:238-252 [6] King J C.Symbolic execution and program testing[J].Communications of the ACM,1976,19(7):385-394 [7] Cadar C,Dunbar D,Engler D R.KLEE:Unassisted and Auto-matic Generation of High-Coverage Tests for Complex Systems Programs[C]∥OSDI.2008,8:209-224 [8] Clang Static Analyzer.http://clang-analyzer.llvm.org/ [9] Dillig I,Dillig T,Aiken A.Sound,complete and scalable path-sensitive analysis[J].ACM SIGPLAN Notices,ACM,2008,43(6):270-280 [10] Llvm I R.LLVM Language Reference Manual.http:// llvm.org/docs/LangRef.html [11] Coreutils.GNU core utilities.http://www.gnu.org /software /coreutils [12] Ganesh V,Dill D L.A decision procedure for bit-vectors and arrays[M]∥Computer Aided Verification.Springer Berlin Heidelberg,2007:519-531 [13] ShapChecker.2015.http://kyhcs.ustcsz.edu.cn /~shape-checker [14] Ku K,Hart T E,Chechik M,et al.A buffer overflow benchmark for software model checkers[C]∥Proceedings of the Twenty-second IEEE/ACM International Conference on Automated Software Engineering.ACM,2007:389-392 [15] Xu Z,Kremenek T,Zhang J.A memory model for static analysis of C programs[M]∥Leveraging Applications of Formal Me-thods,Verification,and Validation.Springer Berlin Heidelberg,2010:535-548 [16] Godefroid P.Compositional dynamic test generation[C]∥Proceedings of POPL.2007 [17] Dillig T.A Modular and Symbolic Approach to Static Program Analysis[D].Palo Alto:Stanford University,2011 |
| No related articles found! |
|
||
首页