Advanced Search
Volume 35 Issue 6
Jun.  2009
Turn off MathJax
Article Contents
Abstract
References
Journal of Beijing University of Aeronautics and Astronautics  > 2009  >  35(6): 687-691.
Liang Jianhong, Luan Yubao, Wang Tianmiao, et al. Design and analysis of four-dimensional force-measurement based on one-dimensional sensors[J]. Journal of Beijing University of Aeronautics and Astronautics, 2013, 39(8): 1011-1015. (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)
shu

Lazy-substitution based symbolic execution for C programs

  • 1.

    State Key Lab. of Software Development Environment, Beijing University of Aeronautics and Astronautics, Beijing 100191,China

  • 2. National Digital Switching Engineering and Technological Research Center, Zhengzhou 450002, China

  • Received Date: 05 May 2008
  • Publish Date: 30 Jun 2009
    Abstract
  • 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.

     

    • FullText(HTML)
    • References(1)
  • [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
    • Relative Articles

  • Relative Articles

    [1]LIU C J，QIAO Z，YAN H W，et al. Semantic segmentation network of remote sensing images based on dual path supervision[J]. Journal of Beijing University of Aeronautics and Astronautics，2025，51（3）：732-741 （in Chinese）. doi: 10.13700/j.bh.1001-5965.2023.0155.
    [2]ZHANG K，LIU Y，HU K. RAW image reconstruction based on multi-scale attention mechanism[J]. Journal of Beijing University of Aeronautics and Astronautics，2025，51（1）：257-264 （in Chinese）. doi: 10.13700/j.bh.1001-5965.2022.0959.
    [3]HOU Z Q，DAI N，CHENG M J，et al. Two-branch real-time semantic segmentation algorithm based on spatial information guidance[J]. Journal of Beijing University of Aeronautics and Astronautics，2025，51（1）：19-29 （in Chinese）. doi: 10.13700/j.bh.1001-5965.2022.0980.
    [4]LIU Sheng, JIN Xuepeng, GAO Feng, GAN Yanhai. Sparse Attention and Deformable Feature Cross Fusion-Based Multi-source Remote Sensing Image Classification Method[J]. Journal of Beijing University of Aeronautics and Astronautics. doi: 10.13700/j.bh.1001-5965.2024.0480
    [5]LIN Sen, CHA Zi-yue. Nighttime image dehazing based on non-uniform atmospheric light correction model[J]. Journal of Beijing University of Aeronautics and Astronautics. doi: 10.13700/j.bh.1001-5965.2023.0437
    [6]SHI Jiliang, ZHANG Qian, ZHOU Zunfu, YANG Sihong. Face Image Inpainting Combining Semantic Segmentation and Edge Texture[J]. Journal of Beijing University of Aeronautics and Astronautics. doi: 10.13700/j.bh.1001-5965.2024.0258
    [7]HU Jianping, GAO Zhipeng, MOU Yang, XIE Qi. Deep learning-based image watermarking combining attack classification and multi-channel embedding[J]. Journal of Beijing University of Aeronautics and Astronautics. doi: 10.13700/j.bh.1001-5965.2024.0552
    [8]LI Lu, CHEN Ke-yan, LIU Chen-yang, SHI Zhen-wei. An anchor-free optical remote sensing image ship detection method[J]. Journal of Beijing University of Aeronautics and Astronautics. doi: 10.13700/j.bh.1001-5965.2023.0852
    [9]JI L N，GUO X M，YANG F B. Adaptive layered fusion algorithm for infrared and visible video based on possibility theory[J]. Journal of Beijing University of Aeronautics and Astronautics，2024，50（10）：3021-3031 （in Chinese）. doi: 10.13700/j.bh.1001-5965.2022.0765.
    [10]DUAN J Z，WANG C J. Sensitivity encoding reconstruction algorithm based on multi-category dictionary learning[J]. Journal of Beijing University of Aeronautics and Astronautics，2024，50（7）：2123-2132 （in Chinese）. doi: 10.13700/j.bh.1001-5965.2022.0571.
    [11]LI H G，WANG Y F，YANG L C. Meta-learning-based few-shot object detection for remote sensing images[J]. Journal of Beijing University of Aeronautics and Astronautics，2024，50（8）：2503-2513 （in Chinese）. doi: 10.13700/j.bh.1001-5965.2022.0637.
    [12]SHAO Wei-zhi, XIONG Si-yu, PAN Li-li. Semi-supervised image retrieval based on triplet hash loss[J]. Journal of Beijing University of Aeronautics and Astronautics. doi: 10.13700/j.bh.1001-5965.2023.0451
    [13]LI Y H，ZHU M Y，REN J，et al. Text-to-image synthesis based on modified deep convolutional generative adversarial network[J]. Journal of Beijing University of Aeronautics and Astronautics，2023，49（8）：1875-1883 （in Chinese）. doi: 10.13700/j.bh.1001-5965.2021.0588.
    [14]GAO Y T，ZHANG J D. Intelligent orbit determination based on remote sensing image of ontology knowledge base[J]. Journal of Beijing University of Aeronautics and Astronautics，2023，49（5）：1053-1062 （in Chinese）. doi: 10.13700/j.bh.1001-5965.2021.0417.
    [15]Ruan Shilong, Dong Zhe, Sun Yao, Qu Xiaolei, Huo Shaoze. Research on Parameter Optimization Method of Thrust Vector/ Pneumatic Rudder Composite Control Law for Aircraft Based on Singular Value Method[J]. Journal of Beijing University of Aeronautics and Astronautics. doi: 10.13700/j.bh.1001-5965.2023.0227
    [16]ZHANG Yi-tian, LUO Xi-ling, WANG Yu-peng. Self-supervised image change detection method based on lightweight capsule network[J]. Journal of Beijing University of Aeronautics and Astronautics. doi: 10.13700/j.bh.1001-5965.2023-0251
    [17]WEN P，CHENG Y L，WANG P，et al. Ground object classification based on height-aware multi-scale graph convolution network[J]. Journal of Beijing University of Aeronautics and Astronautics，2023，49（6）：1471-1478 （in Chinese）. doi: 10.13700/j.bh.1001-5965.2021.0434.
    [18]ZHANG Zhi, YI Hua-hui, ZHENG Jin. Few-Shot Object Detection of Aerial Image Based on Language Guidance Vision[J]. Journal of Beijing University of Aeronautics and Astronautics. doi: 10.13700/j.bh.1001-5965.2023.0491
    [19]ZHOU Z G，WANG J，LI Y，et al. Ultrasonic array testing and evaluation method of multilayer bonded structures[J]. Journal of Beijing University of Aeronautics and Astronautics，2023，49（12）：3207-3214 （in Chinese）. doi: 10.13700/j.bh.1001-5965.2022.0084.
    [20]HU Kai, ZHAO Jian, LIU Yu, NIU Yukai, JI Gang. Images inpainting via structure guidance[J]. Journal of Beijing University of Aeronautics and Astronautics, 2022, 48(7): 1269-1277. doi: 10.13700/j.bh.1001-5965.2021.0004
    • Supplements(0)
    • Cited By
  • Created with Highcharts 5.0.7Amount of accessChart context menuAbstract Views, HTML Views, PDF Downloads StatisticsAbstract ViewsHTML ViewsPDF Downloads2024-052024-062024-072024-082024-092024-102024-112024-122025-012025-022025-032025-0405101520
    Created with Highcharts 5.0.7Chart context menuAccess Class DistributionFULLTEXT: 22.7 %FULLTEXT: 22.7 %META: 76.3 %META: 76.3 %PDF: 1.0 %PDF: 1.0 %FULLTEXTMETAPDF
    Created with Highcharts 5.0.7Chart context menuAccess Area Distribution其他: 2.0 %其他: 2.0 %Seattle: 0.2 %Seattle: 0.2 %上海: 0.5 %上海: 0.5 %佛山: 0.5 %佛山: 0.5 %北京: 2.2 %北京: 2.2 %哥伦布: 0.5 %哥伦布: 0.5 %张家口: 1.5 %张家口: 1.5 %朝阳: 0.5 %朝阳: 0.5 %杭州: 0.2 %杭州: 0.2 %桂林: 0.2 %桂林: 0.2 %武汉: 0.2 %武汉: 0.2 %深圳: 9.8 %深圳: 9.8 %漯河: 0.2 %漯河: 0.2 %芒廷维尤: 10.2 %芒廷维尤: 10.2 %芝加哥: 0.2 %芝加哥: 0.2 %西宁: 69.8 %西宁: 69.8 %西安: 0.2 %西安: 0.2 %达州: 0.5 %达州: 0.5 %郑州: 0.5 %郑州: 0.5 %其他Seattle上海佛山北京哥伦布张家口朝阳杭州桂林武汉深圳漯河芒廷维尤芝加哥西宁西安达州郑州

Catalog

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

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

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

    Article Metrics

    Article views(3287) PDF downloads(1646) Cited by()
    Proportional views
    Related

    Copyright © Journal of Beijing University of Aeronautics and Astronautics

    Address: Editorial Department of Journal of Beijing University of Aeronautics and Astronautics, 37 Xueyuan Road, Haidian District, Beijing Post Code: 100191 Email: jbuaa@buaa.edu.cn

    Supported by: Beijing Renhe Information Technology Co., Ltd.    

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return