SYMBOLIC EXECUTION IN AUTOMATICALLY GENERATIONOF DATA OF SOFTWARE TESTING
DOI:
https://doi.org/10.37569/DalatUniversity.6.2.44(2016)Keywords:
Constraint solving, Dynamic symbolic execution, Symbolic execution, Testing data, Testing data generation.Abstract
In software testing area, all test cases are often generated manually. It time-consumming and costly to complete such task. Symbolic execution is a well-known technique for automatically making the test cases that cover almost every testing criteria in order to deeply discover some errors in complex software systems. In this paper, we present some general points and several results in recent researches about symbolic execution technique. This paper also shows different challenges that need setting in this field such as the explosion of execution paths in a program, the ability of constraint solving, memory modelling or concurrent problems etc. The evaluation of published results is given in this paper as well.
Metrics
References
R. S. Boyer, B. Elspas, and K. N. Levitt. SELECT – a formal system for testing and debugging programs by symbolic execution. SIGPLAN Not., 10:234–245, (1975).
A. I. Baars, M. Harman, Y. Hassoun, K. Lakhotia, P. McMinn, P. Tonella, and T. E. J. Vos. Symbolic search-based testing. In ASE’11, (2011).
H. Zhu, P. Hall, J. May. Software Unit Test Coverage and Adequacy. ACM Computing Surveys, 29 (4). ISSN 0360-0300, December, pp. 366–427, (1997).
C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI’08, Dec (2008).
J. Burnim and K. Sen. Heuristics for scalable dynamic test generation. In ASE’08, Sept. (2008).
D. Bird and C. Munoz, “Automatic Generation of Random Self- Checking Test Cases,” IBM Systems Journal, vol. 22, no. 3, pp. 229–245, (1983).
C. Cadar and D. Engler. Execution generated test cases: How to make systems code crash itself (invited paper). In SPIN’05, Aug (2005).
C. Cadar, V. Ganesh, P. Pawlowski, D. Dill, and D. Engler. EXE: Automatically generating inputs of death. In CCS’06, Oct–Nov 2006. An extended version appeared in ACM TISSEC 12:2, (2008).
] P. Collingbourne, C. Cadar, and P. H. Kelly. Symbolic crosschecking of floating-point and SIMD code. In EuroSys’11, Apr (2011).
L. A. Clarke. A program testing system. In Proc. of the 1976 annual conference, pages 488–491, (1976).
L. De Moura and N. Bjorner. Satisfiability modulo theories: introduction and applications. Commun. ACM, 54:69–77, Sept. (2011).
B. Elkarablieh, P. Godefroid, and M. Y. Levin. Precise pointer reasoning for dynamic test generation. In ISSTA’09, (2009).
V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In CAV’07, July (2007).
P. Godefroid. Compositional dynamic test generation. In POPL’07, Jan. (2007).
P. Godefroid. Higher-order test generation. In PLDI’11, (2011).
P. Godefroid, N. Klarlund, and K. Sen. DART: Directed Automated Random Testing. In PLDI’05, June (2005).
P. Godefroid, M. Levin, and D. Molnar. Automated Whitebox Fuzz Testing. In NDSS’08, Feb. (2008).
W. Howden. Symbolic testing and the DISSECT symbolic evaluation system. IEEE Transactions on Software Engineering, 3(4):266–278, (1977).
K. Inkumsah and T. Xie. Improving structural testing of object-oriented programs via integrating evolutionary testing and symbolic execution. In ASE’08, (2008).
Y. Jia and M. Harman. An analysis and survey of the development of mutation testing. IEEE Trans. Software Eng., 37(5):649–678, (2011).
J. C. King. Symbolic execution and program testing. Commun. ACM, 9:385–394, July (1976).
K. Lakhotia, P. McMinn, and M. Harman. An empirical investigation into branch coverage for C programs using CUTE and AUSTIN. J. Systems and Software, 83(12):2379–91, (2010).
R. Majumdar and K. Sen. Latest: Lazy dynamic test input generation. Technical Report UCB/EECS-2007-36, EECS Department, University of California, Berkeley, Mar (2007).
K. Sen and G. Agha. Automated systematic testing of open distributed programs. In FASE’06, (2006).
K. Sen and G. Agha. CUTE and jCUTE : Concolic unit testing and explicit path model-checking tools. In CAV’06, (2006).
K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. In ESEC/FSE’05, Sep (2005).
T. Xie, N. Tillmann, J. de Halleux, and W. Schulte. Fitnessguided path exploration in dynamic symbolic execution. In DSN’09, pages 359–368, (2009).
N. Tillmann and J. de Halleux. Pex - white box test generation for .NET. In TAP’08, Apr (2008).
R. S. Boyer, B. Elspas, and K. N. Levitt. SELECT – a formal system for testing and debugging programs by symbolicexecution. SIGPLAN Not., 10:234–245, (1975).
C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI’08, Dec (2008).Web site
http://msdn2.microsoft.com/vs2008/
http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc
Downloads
Published
Volume and Issues
Section
Copyright & License
Copyright (c) 2016 Tô Hữu Nguyên, Nguyễn Hồng Tân, Hà Thị Thanh, Đỗ Thanh Mai
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
How to Cite
