Volume 35 Issue 6
Jun.  2009
Turn off MathJax
Article Contents
Lin Mengxiang, Chen Yinli, Chen Rui, et al. Lazy-substitution based symbolic execution for C programs[J]. Journal of Beijing University of Aeronautics and Astronautics, 2009, 35(6): 687-691. (in Chinese)
Citation: Lin Mengxiang, Chen Yinli, Chen Rui, et al. Lazy-substitution based symbolic execution for C programs[J]. Journal of Beijing University of Aeronautics and Astronautics, 2009, 35(6): 687-691. (in Chinese)

Lazy-substitution based symbolic execution for C programs

  • Received Date: 05 May 2008
  • Publish Date: 30 Jun 2009
  • Lazy-substitution based symbolic execution was presented in order to address the computed memory location problem in traditional symbolic execution. A form of lazy strategy was introduced into traditional symbolic execution, which substitutes program variables with their symbolic values as much as possible. When the memory locations of variables in a statement can-t be determined statically or the length of a symbolic expression for substitution is too long, those variables won-t be replaced with their symbolic values. The lazy substitution algorithm was provided. Moreover, the lazy symbolic execution semantics for most of structures in C programming language were discussed in detail, especially for array and pointer. The prototype of symbolic execution system LazySEC (a lazy symbolic executor for C programs) performs lazy-substitution based symbolic execution for C programs. Preliminary experiment results show that LazySEC can handle program structures involving computed memory locations efficiently.

     

  • loading
  • [1] King J C. Symbolic execution and program testing [J]. Commun ACM,1976,19(7):385-394 [2] Godefroid P, Klarlund N, Sen K. DART: Directed automated random testing ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI-05). New York:ACM,2005:213-223 [3] Godefroid P. Compositional dynamic test generation 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL-07). New York: ACM, 2007:47-54 [4] Coen-Porisini A, Denaro G, Ghezzi C, et al. Using symbolic execution for verifying safety-critical systems 8th European Software Engineering Conference. New York: ACM, 2001:142-151 [5] 单锦辉, 王戟, 齐治昌. 面向路径的测试数据自动生成方法述评[J]. 电子学报, 2004, 32(1):109-113 Shan Jinhui, Wang Ji, Qi Zhichang. Survey on path-wise automatic generation of test data[J]. Acta Electronica Sinica,2004,32(1):109-113(in Chinese) [6] Boyer R S, Elspas B, Levitt K N. SELECT-a formal system for testing and debugging programs by symbolic execution Proceeding of the International Conference on Reliable Software. New York: ACM, 1975:234-245 [7] Clarke L A. A system to generate test data and symbolically execute programs [J]. IEEE Transactions Software Engineering, 1976, SE-2(3):215-222 [8] Ramamoorthy C V, Ho S B, Chen W T. On the automated generation of program test data [J]. IEEE Transactions on Software Engineering, 1976, SE-2(4):293-300 [9] Zhang Jian, Wang Xiaoxu. A constraint solver and its application to path feasibility analysis [J]. International Journal of Software Engineering and Knowledge Engineering,2001,11(2):139-156 [10] Zhang Jian. Symbolic execution of program paths involving pointer and structure variables Proc of the Fourth Int Conf on Quality Software (QSIC-04). Los Alamitos: IEEE Computer Society, 2004:87-92 [11] Khurshid S, Pasareanu C, Visser W. Generalized symbolic execution for model checking and testing Tools and Algorithms for Construction and Analysis of Systems (TACAS’03). Heidelberg: Springer, 2003:553-568 [12] Coward P D. Symbolic execution and testing [J]. Information and Software Technology,1991,33(1):53-64
  • 加载中

Catalog

    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Article Metrics

    Article views(3193) PDF downloads(1643) Cited by()
    Proportional views
    Related

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return