[an error occurred while processing this directive]
���¿��ټ��� �߼�����
   ��ҳ  �ڿ�����  ��ί��  Ͷ��ָ��  �ڿ�����  ��������  �� �� ��  ��ϵ����
�������պ����ѧѧ�� 2009, Vol. 35 Issue (6) :687-691    DOI:
���� ����Ŀ¼ | ����Ŀ¼ | ������� | �߼����� << | >>
������1, ��ط��1, �� �1, �� ��2*
1. �������պ����ѧ ����������������ص�ʵ����, ���� 100191;
2. �������ݽ���ϵͳ���̼����о�����, ֣�� 450002
Lazy-substitution based symbolic execution for C programs
Lin Mengxiang1, Chen Yinli1, Chen Rui1, Zhou Gang2*
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

Download: PDF (0KB)   HTML 1KB   Export: BibTeX or EndNote (RIS)      Supporting Info
ժҪ ��Դ�ͳ����ִ���еĶ�̬��ַ��������,����˻������滻�ķ���ִ�з���.ͨ�����뾡�����滻�IJ���,�������滻�ķ���ִ�����޷���̬ȷ�������ĵ�ַ����ű��ʽ����ʱ���������滻.���ȸ����˻������滻�ķ���ִ���㷨,�ڴ˻�����,��ϸ������C������Ҫ�ṹ�����������ָ���������ִ������.LazySEC��һ������C�����������ִ��ϵͳԭ��,����ʵ�����,��������Ч�ش�����ָ��ͽṹ����漰��̬��ַ����ij������Խṹ.
Email Alert
�ؼ����� �������   �������   ����     
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.
Keywords�� software engineering   program debugging   tools     
Received 2008-05-05;


About author: ������(1968-),Ů,����������,��ʿ��,mxlin@nlsde.buaa.edu.cn.
������, ��ط��, �� �, �� ��.�������滻��C����ִ��[J]  �������պ����ѧѧ��, 2009,V35(6): 687-691
Lin Mengxiang, Chen Yinli, Chen Rui, Zhou Gang.Lazy-substitution based symbolic execution for C programs[J]  JOURNAL OF BEIJING UNIVERSITY OF AERONAUTICS AND A, 2009,V35(6): 687-691
http://bhxb.buaa.edu.cn//CN/     ��     http://bhxb.buaa.edu.cn//CN/Y2009/V35/I6/687
Copyright 2010 by �������պ����ѧѧ��