Abstract
Loops can represent an infinite number of possible execution paths and therefore purse a major challenge for current static analysis frameworks and test input generators. In this paper, we introduce a new loop exploration algorithm to examine different iteration orders (i.e. loop paths) in order to test distinct loop behaviour. To reduce the complexity of testing all possible combinations of iterations, we introduce a criterion to group different paths into equivalence classes and show how to specifically generate test cases that cover the different equivalence classes. We demonstrate how this approach helps to achieve higher coverage rates and helps to find software failures that are not discovered by current test case generation frameworks.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Xiao, X., Li, S., Xie, T., Tillmann, N.: Characteristic studies of loop problems for structural test generation via symbolic execution. In: Proceedings of 28th IEEE/ACM International Conference on Automated Software Engineering (ASE 2013), November 2013
Liu, T., Nagel, M., Taghdiri, M.: Bounded program verification using an SMT solver: a case study. In: 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation (ICST), pp. 101–110. IEEE (2012)
Godefroid, P., Levin, M.Y., Molnar, D.A., et al.: Automated whitebox fuzz testing. In: NDSS, vol. 8, pp. 151–166 (2008)
D’silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 27(7), 1165–1178 (2008)
Cok, D.R., Kiniry, J.R.: ESC/Java2: uniting ESC/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108–128. Springer, Heidelberg (2005)
Blanc, R., Kuncak, V., Kneuss, E., Suter, P.: An overview of the Leon verification system: verification by translation to recursive functions. In: Proceedings of the 4th Workshop on Scala, p. 1. ACM (2013)
Francis, K., Stuckey, P.J.: Loop untangling. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 340–355. Springer, Heidelberg (2014)
Williams, N., Marre, B., Mouy, P., Roger, M.: PathCrawler: automatic generation of path tests by combining static and dynamic analysis. In: Dal Cin, M., Kaâniche, M., Pataricza, A. (eds.) EDCC 2005. LNCS, vol. 3463, pp. 281–292. Springer, Heidelberg (2005)
Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. SIGPLAN Not. 40(6), 213–223 (2005). DirectedTesting
Xie, T., Tillmann, N., de Halleux, J., Schulte, W.: Fitness-guided path exploration in dynamic symbolic execution. In: IEEE/IFIP International Conference on Dependable Systems Networks, DSN 2009, pp. 359–368, June 2009
Obdržálek, J., Trtík, M.: Efficient loop navigation for symbolic execution. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 453–462. Springer, Heidelberg (2011)
Godefroid, P., Luchaup, D.: Automatic partial loop summarization in dynamic test generation. In: Proceedings of the 2011 International Symposium on Software Testing and Analysis, ISSTA 2011, pp. 23–33. ACM, New York (2011)
Donaldson, A.F., Haller, L., Kroening, D., Rümmer, P.: Software verification using k-induction. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 351–368. Springer, Heidelberg (2011)
Tsitovich, A., Sharygina, N., Wintersteiger, C.M., Kroening, D.: Loop summarization and termination analysis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 81–95. Springer, Heidelberg (2011)
Louhichi, A., Ghardallou, W., Bsaies, K., Jilani, L.L., Mraihi, O., Mili, A.: Verifying while loops with invariant relations. Int. J. Crit. Comput.-Based Syst. 5(1), 78–102 (2014)
Kroning, D., Groce, A., Clarke, E.: Counterexample guided abstraction refinement via program execution. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 224–238. Springer, Heidelberg (2004)
Kroening, D., Weissenbacher, G.: Verification and falsification of programs with loops using predicate abstraction. Formal Aspects Comput. 22(2), 105–128 (2010)
Godefroid, P., de Halleux, P., Nori, A.V., Rajamani, S.K., Schulte, W., Tillmann, N., Levin, M.Y.: Automating software testing using program analysis. IEEE Softw. 25(5), 30–37 (2008)
Lee, G., Morris, J., Parker, K., Bundell, G.A., Lam, P.: Using symbolic execution to guide test generation. Softw. Test. Verification Reliab. 15(1), 41–61 (2005)
de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Huster, S. et al. (2015). Efficient Testing of Different Loop Paths. In: Calinescu, R., Rumpe, B. (eds) Software Engineering and Formal Methods. SEFM 2015. Lecture Notes in Computer Science(), vol 9276. Springer, Cham. https://doi.org/10.1007/978-3-319-22969-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-22969-0_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-22968-3
Online ISBN: 978-3-319-22969-0
eBook Packages: Computer ScienceComputer Science (R0)