Computer Science ›› 2016, Vol. 43 ›› Issue (3): 193-198.doi: 10.11896/j.issn.1002-137X.2016.03.036
Previous Articles Next Articles
LIANG Jia-biao, LI Zhao-peng, ZHU Ling and SHEN Xian-fei
[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! |
|