Computer Science ›› 2016, Vol. 43 ›› Issue (3): 193-198.doi: 10.11896/j.issn.1002-137X.2016.03.036

Previous Articles     Next Articles

Symbolic Execution Engine with Shape Analysis

LIANG Jia-biao, LI Zhao-peng, ZHU Ling and SHEN Xian-fei   

  • Online:2018-12-01 Published:2018-12-01

Abstract: Dynamic testing,static analysis and formal verification are three major methods for improving the depen-dability 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.

Key words: Symbolic execution,Static analysis,Loop invariant,Recursive function

[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!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!