×

Strategies for scalable symbolic execution-driven test generation for programs. (English) Zbl 1267.68094

Summary: With the advent of advanced program analysis and constraint solving techniques, several test generation tools use variants of symbolic execution. Symbolic techniques have been shown to be very effective in path-based test generation; however, they fail to scale to large programs due to the exponential number of paths to be explored. In this paper, we focus on tackling this path explosion problem and propose search strategies to achieve quick branch coverage under symbolic execution, while exploring only a fraction of paths in the program. We present a reachability-guided strategy that makes use of the reachability graph of the program to explore unvisited portions of the program and a conflict-driven backtracking strategy that utilizes conflict analysis to perform nonchronological backtracking. We present experimental evidence that these strategies can significantly reduce the search space and improve the speed of test generation for programs.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Myers G J. Art of Software Testing. New York: John Wiley & Sons, Inc., 1979 · Zbl 0782.68002
[2] Sen K. Marinov D, Agha G. CUTE: A concolic unit testing engine for C. In: Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, New York, NY, USA, 2005. 263–272
[3] Pacheco C, Ernst M D. Eclat: Automatic generation and classification of test inputs. In: Proceedings of the 19th European Conference Object-Oriented Programming, Glasgow, UK, 2005. 504–527
[4] Godefroid P, Klarlund N, Sen K. DART: Directed automated random testing. In: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design And Implementation, New York, NY, USA, 2005. 213–223
[5] Coward P D. Symbolic execution systems–a review. Softw Eng J, 1988, 3: 229–239 · doi:10.1049/sej.1988.0029
[6] Burnim J, Sen K. Heuristics for scalable dynamic test generation. In: Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering, L’Aquila, Italy, 2008. 443–446
[7] Boonstoppel P, Cadar C, Engler D R. RWset: Attacking path explosion in constraint-based test generation. In: Proceedings of the 14th International Conference on Tools and Algorithms for Construction and Analysis of Systems, Budapest, Hungary, 2008. 351–366
[8] Technology B T. Who is Using BullseyeCoverage. http://www.bullseye.com/successWho.html
[9] Technology B T. BullseyeCoverage-Measurement Technique. http://www.bullseye.com/measurementTechnique.html
[10] Bardin S, Herrmann P. Pruning the search space in path-based test generation. In: Proceedings of the 2009 International Conference on Software Testing Verification and Validation, Washington DC, USA, 2009. 240–249
[11] Majumdar R, Sen K. Hybrid concolic testing. In: Proceedings of the 29th International Conference on Software Engineering, Minneapolis, MN, USA, 2007. 416–426
[12] Cadar C, Ganesh V, Pawlowski P, et al. EXE: Automatically generating inputs of death. ACM Trans Inf Syst Secur, 2008, 12: 10
[13] Godefroid P, Levin M, Molnar D, et al. Automated whitebox fuzz testing. In: Proceedings of the Network and Distributed System Security Symposium, San Diego, CA, USA, 2008
[14] Godefroid P. Compositional dynamic test generation. In: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, NY, USA, 2007. 47–54
[15] Anand S, Godefroid P, Tillmann N. Demand-Driven Compositional Symbolic Execution. Technical Report MSR-TR 2007-138. 2008 · Zbl 1134.68355
[16] Marques-Silva J, Sakallah K. GRASP: A search algorithm for propositional satisfiability. IEEE Trans Comput, 1999, 48: 506–521 · Zbl 01935259 · doi:10.1109/12.769433
[17] Ranise S, Tinelli C. The SMT-LIB Standard: Version 1.2. Technical Report, Department of Computer Science, The University of Iowa. 2006
[18] Barrett C, Berezin S. CVC Lite: A new implementation of the cooperating validity checker category b. In: Computer Aided Verification. New York: Springer, 2004. 19–21
[19] Bruttomesso R, Cimatti A, Franzén A, et al. The Mathsat 4 SMT solver. In: Computer Aided Verification. New York: Springer, 2008. 299–303
[20] Dutertre B, De Moura L. The Yices SMT Solver. Tool paper at http://yices.csl.sri.com/tool-paper.pdf , 2006
[21] Dutertre B, De Moura L. A fast linear-arithmetic solver for DPLL (T). In: Computer Aided Verification. New York: Springer, 2006. 81–94
[22] Necula G C, McPeak S, Rahul S P, et al. CIL: Intermediate language and tools for analysis and transformation of C programs. In: Proceedings of the 11th International Conference on Compiler Construction, London, UK, 2002. 213–228 · Zbl 1051.68756
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.